let D be non empty set ; for i being natural Number
for T1, T2, T3 being Tuple of i,D
for F being BinOp of D st F is associative holds
F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
let i be natural Number ; for T1, T2, T3 being Tuple of i,D
for F being BinOp of D st F is associative holds
F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
let T1, T2, T3 be Tuple of i,D; for F being BinOp of D st F is associative holds
F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
let F be BinOp of D; ( F is associative implies F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3))) )
assume A1:
F is associative
; F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))
per cases
( i = 0 or i <> 0 )
;
suppose A2:
i = 0
;
F .: ((F .: (T1,T2)),T3) = F .: (T1,(F .: (T2,T3)))then
F .: (
T1,
T2)
= <*> D
by Lm1;
then A3:
F .: (
(F .: (T1,T2)),
T3)
= <*> D
by FINSEQ_2:73;
F .: (
T2,
T3)
= <*> D
by A2, Lm1;
hence
F .: (
(F .: (T1,T2)),
T3)
= F .: (
T1,
(F .: (T2,T3)))
by A3, FINSEQ_2:73;
verum end; end;