∀ x y z, (x × (y × z)) = (y × (x × z))

Theorem times_times : forall (x:nat), forall (y:nat), forall (z:nat), logic.eq (nat) (times x (times y z)) (times y (times x z)).

theorem times_times : \forall (x:nat). \forall (y:nat). \forall (z:nat). (eq) (nat) ((times) x ((times) y z)) ((times) y ((times) x z)).

theorem times_times : forall (x:nat.nat) , forall (y:nat.nat) , forall (z:nat.nat) , (((logic.eq_) (nat.nat)) ((((nat.times) ) (x)) ((((nat.times) ) (y)) (z)))) ((((nat.times) ) (y)) ((((nat.times) ) (x)) (z))).

times_times : LEMMA (FORALL(x:nat_sttfa.sttfa_nat):(FORALL(y:nat_sttfa.sttfa_nat):(FORALL(z:nat_sttfa.sttfa_nat):logic_sttfa_th.eq[nat_sttfa.sttfa_nat](nat_sttfa.times(x)(nat_sttfa.times(y)(z)))(nat_sttfa.times(y)(nat_sttfa.times(x)(z))))))

Printing for OpenTheory is not working at the moment.