let D be non empty set ; :: thesis: for S being non empty Subset of
for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
let S be non empty Subset of ; :: thesis: for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
let f be BinOp of D; :: thesis: for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
let g be BinOp of S; :: thesis: ( g = f || S implies ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) )
A1: dom g = [:S,S:] by FUNCT_2:def 1;
assume A2: g = f || S ; :: thesis: ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
thus ( f is commutative implies g is commutative ) :: thesis: ( ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )

proof

assume A3: for a, b being Element of D holds f . a,b = f . b,a ; :: according to BINOP_1:def 13 :: thesis: g is commutative
let a, b be Element of S; :: according to BINOP_1:def 13 :: thesis: g . a,b = g . b,a
reconsider a' = a, b' = b as Element of S ;
reconsider a' = a', b' = b' as Element of D ;
thus g . a,b = f . [a,b] by A2, A1, FUNCT_1:70
.= f . a',b'
.= f . b',a' by A3
.= g . [b,a] by A2, A1, FUNCT_1:70
.= g . b,a ; :: thesis: verum

end;

thus ( f is idempotent implies g is idempotent ) :: thesis: ( f is associative implies g is associative )

proof

assume A4: for a being Element of D holds f . a,a = a ; :: according to BINOP_1:def 15 :: thesis: g is idempotent
let a be Element of S; :: according to BINOP_1:def 15 :: thesis: g . a,a = a
thus g . a,a = f . [a,a] by A2, A1, FUNCT_1:70
.= f . a,a
.= a by A4 ; :: thesis: verum

end;

assume A5: for a, b, c being Element of D holds f . (f . a,b),c = f . a,(f . b,c) ; :: according to BINOP_1:def 14 :: thesis: g is associative
let a, b, c be Element of S; :: according to BINOP_1:def 14 :: thesis: g . a,(g . b,c) = g . (g . a,b),c
reconsider a' = a, b' = b, c' = c as Element of S ;
reconsider a' = a', b' = b', c' = c' as Element of D ;
thus g . (g . a,b),c = f . [(g . a,b),c] by A2, A1, FUNCT_1:70
.= f . [(f . [a,b]),c] by A2, A1, FUNCT_1:70
.= f . (f . a,b),c
.= f . a',(f . b',c') by A5
.= f . a,(g . [b,c]) by A2, A1, FUNCT_1:70
.= f . [a,(g . b,c)]
.= g . a,(g . b,c) by A2, A1, FUNCT_1:70 ; :: thesis: verum