let D be non empty set ; for F being BinOp of D
for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
let F be BinOp of D; for i being Nat
for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
let i be Nat; for T1, T2 being Element of i -tuples_on D st F is commutative & F is associative & F is having_a_unity holds
F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2))
let T1, T2 be Element of i -tuples_on D; ( F is commutative & F is associative & F is having_a_unity implies F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2)) )
( len T1 = i & len T2 = i )
by CARD_1:def 7;
hence
( F is commutative & F is associative & F is having_a_unity implies F . ((F "**" T1),(F "**" T2)) = F "**" (F .: (T1,T2)) )
by Th34; verum