let D be non empty set ; :: thesis: for d1, d2 being Element of D

for F being BinOp of D

for i being Nat st F is commutative & F is associative & F is having_a_unity holds

F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))

let d1, d2 be Element of D; :: thesis: for F being BinOp of D

for i being Nat st F is commutative & F is associative & F is having_a_unity holds

F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))

let F be BinOp of D; :: thesis: for i being Nat st F is commutative & F is associative & F is having_a_unity holds

F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))

let i be Nat; :: thesis: ( F is commutative & F is associative & F is having_a_unity implies F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2))) )

reconsider T1 = i |-> d1, T2 = i |-> d2 as Element of i -tuples_on D ;

i |-> (F . (d1,d2)) = F .: (T1,T2) by FINSEQOP:17;

hence ( F is commutative & F is associative & F is having_a_unity implies F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2))) ) by Th35; :: thesis: verum

for F being BinOp of D

for i being Nat st F is commutative & F is associative & F is having_a_unity holds

F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))

let d1, d2 be Element of D; :: thesis: for F being BinOp of D

for i being Nat st F is commutative & F is associative & F is having_a_unity holds

F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))

let F be BinOp of D; :: thesis: for i being Nat st F is commutative & F is associative & F is having_a_unity holds

F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2)))

let i be Nat; :: thesis: ( F is commutative & F is associative & F is having_a_unity implies F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2))) )

reconsider T1 = i |-> d1, T2 = i |-> d2 as Element of i -tuples_on D ;

i |-> (F . (d1,d2)) = F .: (T1,T2) by FINSEQOP:17;

hence ( F is commutative & F is associative & F is having_a_unity implies F "**" (i |-> (F . (d1,d2))) = F . ((F "**" (i |-> d1)),(F "**" (i |-> d2))) ) by Th35; :: thesis: verum