let D1, D2 be non empty set ; :: thesis: for a1 being Element of D1
for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let a1 be Element of D1; :: thesis: for a2 being Element of D2
for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let a2 be Element of D2; :: thesis: for f1 being BinOp of D1
for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds
( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
let f2 be BinOp of D2; :: thesis: ( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| )
thus ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 implies [a1,a2] is_a_unity_wrt |:f1,f2:| ) :: thesis: ( [a1,a2] is_a_unity_wrt |:f1,f2:| implies ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) )

proof

assume ( a1 is_a_left_unity_wrt f1 & a1 is_a_right_unity_wrt f1 & a2 is_a_left_unity_wrt f2 & a2 is_a_right_unity_wrt f2 ) ; :: according to BINOP_1:def 7 :: thesis: [a1,a2] is_a_unity_wrt |:f1,f2:|
hence ( [a1,a2] is_a_left_unity_wrt |:f1,f2:| & [a1,a2] is_a_right_unity_wrt |:f1,f2:| ) by Th25, Th26; :: according to BINOP_1:def 7 :: thesis: verum

end;

assume ( [a1,a2] is_a_left_unity_wrt |:f1,f2:| & [a1,a2] is_a_right_unity_wrt |:f1,f2:| ) ; :: according to BINOP_1:def 7 :: thesis: ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 )
hence ( a1 is_a_left_unity_wrt f1 & a1 is_a_right_unity_wrt f1 & a2 is_a_left_unity_wrt f2 & a2 is_a_right_unity_wrt f2 ) by Th25, Th26; :: according to BINOP_1:def 7 :: thesis: verum