let D be non empty set ; :: thesis: for S being non empty Subset of D
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 D; :: 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 2 :: thesis: g is commutative
let a, b be Element of S; :: according to BINOP_1:def 2 :: thesis: g . (a,b) = g . (b,a)
reconsider a9 = a, b9 = b as Element of S ;
reconsider a9 = a9, b9 = b9 as Element of D ;
thus g . (a,b) = f . [a,b] by A2, A1, FUNCT_1:47
.= f . (a9,b9)
.= f . (b9,a9) by A3
.= g . [b,a] by A2, A1, FUNCT_1:47
.= 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 4 :: thesis: g is idempotent
let a be Element of S; :: according to BINOP_1:def 4 :: thesis: g . (a,a) = a
thus g . (a,a) = f . [a,a] by A2, A1, FUNCT_1:47
.= 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 3 :: thesis: g is associative
let a, b, c be Element of S; :: according to BINOP_1:def 3 :: thesis: g . (a,(g . (b,c))) = g . ((g . (a,b)),c)
reconsider a9 = a, b9 = b, c9 = c as Element of S ;
reconsider a9 = a9, b9 = b9, c9 = c9 as Element of D ;
thus g . ((g . (a,b)),c) = f . [(g . (a,b)),c] by A2, A1, FUNCT_1:47
.= f . [(f . [a,b]),c] by A2, A1, FUNCT_1:47
.= f . ((f . (a,b)),c)
.= f . (a9,(f . (b9,c9))) by A5
.= f . (a,(g . [b,c])) by A2, A1, FUNCT_1:47
.= f . [a,(g . (b,c))]
.= g . (a,(g . (b,c))) by A2, A1, FUNCT_1:47 ; :: thesis: verum