let A, C be non empty set ; :: thesis: for L being commutative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is commutative
let L be commutative BinOp of A; :: thesis: for LC being BinOp of C st C c= A & LC = L || C holds
LC is commutative
let LC be BinOp of C; :: thesis: ( C c= A & LC = L || C implies LC is commutative )
assume Z1: ( C c= A & LC = L || C ) ; :: thesis: LC is commutative
for a, b being Element of C holds LC . (a,b) = LC . (b,a)

proof

let a, b be Element of C; :: thesis: LC . (a,b) = LC . (b,a)
reconsider aa = a, bb = b as Element of A by Z1;
ZZ: L . (aa,bb) = L . (bb,aa) by BINOP_1:def 2;
thus LC . (a,b) = L . [aa,bb] by ZFMISC_1:87, FUNCT_1:49, Z1
.= LC . (b,a) by ZZ, ZFMISC_1:87, FUNCT_1:49, Z1 ; :: thesis: verum

end;

hence LC is commutative by BINOP_1:def 2; :: thesis: verum