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:70
.= 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:70
.= 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

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:70
.= s by A6, BINOP_1:11 ;
:: thesis: g . s,d9 = s
[s,d9] in [:S,S:] ;
hence g . s,d9 = f . s9,d by A1, A2, A7, FUNCT_1:70
.= s by A6, BINOP_1:11 ;
:: thesis: verum

end;

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