let A, C be non empty set ; for L being associative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is associative
let L be associative BinOp of A; for LC being BinOp of C st C c= A & LC = L || C holds
LC is associative
let LC be BinOp of C; ( C c= A & LC = L || C implies LC is associative )
assume Z1:
( C c= A & LC = L || C )
; LC is associative
A1:
dom LC = [:C,C:]
by FUNCT_2:def 1;
for a, b, c being Element of C holds LC . (a,(LC . (b,c))) = LC . ((LC . (a,b)),c)
proof
let a,
b,
c be
Element of
C;
LC . (a,(LC . (b,c))) = LC . ((LC . (a,b)),c)
reconsider aa =
a,
bb =
b,
cc =
c as
Element of
A by Z1;
W2:
LC . (
aa,
bb)
= L . (
a,
b)
by ZFMISC_1:87, FUNCT_1:49, Z1;
ZZ:
L . (
aa,
(L . (bb,cc)))
= L . (
(L . (aa,bb)),
cc)
by BINOP_1:def 3;
set y =
[aa,(LC . [bb,cc])];
thus LC . (
a,
(LC . (b,c))) =
L . [aa,(LC . [bb,cc])]
by FUNCT_1:49, Z1, ZFMISC_1:87
.=
L . (
(L . (aa,bb)),
cc)
by ZZ, ZFMISC_1:87, FUNCT_1:49, Z1
.=
LC . (
(LC . (a,b)),
c)
by FUNCT_1:47, A1, Z1, W2, ZFMISC_1:87
;
verum
end;
hence
LC is associative
by BINOP_1:def 3; verum