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 that
A1: a1 is_a_left_unity_wrt f1 and
A2: a1 is_a_right_unity_wrt f1 and
A3: a2 is_a_left_unity_wrt f2 and
A4: a2 is_a_right_unity_wrt f2 ; :: according to BINOP_1:def 7 :: thesis: [a1,a2] is_a_unity_wrt |:f1,f2:|
thus ( [a1,a2] is_a_left_unity_wrt |:f1,f2:| & [a1,a2] is_a_right_unity_wrt |:f1,f2:| ) by A1, A2, A3, A4, Th25, Th26; :: according to BINOP_1:def 7 :: thesis: verum

end;

assume that
A5: [a1,a2] is_a_left_unity_wrt |:f1,f2:| and
A6: [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 )
thus ( 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 A5, A6, Th25, Th26; :: according to BINOP_1:def 7 :: thesis: verum