let A, C be non empty set ; 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; for LC being BinOp of C st C c= A & LC = L || C holds
LC is commutative
let LC be BinOp of C; ( C c= A & LC = L || C implies LC is commutative )
assume Z1:
( C c= A & LC = L || C )
; 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;
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
;
verum
end;
hence
LC is commutative
by BINOP_1:def 2; verum