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
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let S be non empty Subset of D; :: thesis: for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let f be BinOp of D; :: thesis: for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let g be BinOp of S; :: thesis: for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let d be Element of D; :: thesis: for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let d9 be Element of S; :: thesis: ( g = f || S & d9 = d implies ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) )
assume that
A1: g = f || S and
A2: d9 = d ; :: thesis: ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
A3: dom g = [:S,S:] by FUNCT_2:def 1;
thus ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) :: thesis: ( ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )

proof

assume A4: for a being Element of D holds f . (d,a) = a ; :: according to BINOP_1:def 16 :: thesis: d9 is_a_left_unity_wrt g
let a be Element of S; :: according to BINOP_1:def 16 :: thesis: g . (d9,a) = a
thus g . (d9,a) = f . [d9,a] by A1, A3, FUNCT_1:47
.= f . (d,a) by A2
.= a by A4 ; :: thesis: verum

end;

thus ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) :: thesis: ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g )

proof

assume A5: for a being Element of D holds f . (a,d) = a ; :: according to BINOP_1:def 17 :: thesis: d9 is_a_right_unity_wrt g
let a be Element of S; :: according to BINOP_1:def 17 :: thesis: g . (a,d9) = a
thus g . (a,d9) = f . [a,d9] by A1, A3, FUNCT_1:47
.= f . (a,d) by A2
.= a by A5 ; :: thesis: verum

end;

assume A6: d is_a_unity_wrt f ; :: thesis: d9 is_a_unity_wrt g

now :: thesis: for s being Element of S holds
( g . (d9,s) = s & g . (s,d9) = s )

let s be Element of S; :: thesis: ( g . (d9,s) = s & g . (s,d9) = s )
reconsider s9 = s as Element of D ;
A7: dom g = [:S,S:] by FUNCT_2:def 1;
[d9,s] in [:S,S:] ;
hence g . (d9,s) = f . (d,s9) by A1, A2, A7, FUNCT_1:47
.= s by A6, BINOP_1:3 ;
:: thesis: g . (s,d9) = s
[s,d9] in [:S,S:] ;
hence g . (s,d9) = f . (s9,d) by A1, A2, A7, FUNCT_1:47
.= s by A6, BINOP_1:3 ;
:: thesis: verum

end;

hence d9 is_a_unity_wrt g by BINOP_1:3; :: thesis: verum