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

now

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

end;

hence d' is_a_unity_wrt g by BINOP_1:11; :: thesis: verum