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_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_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_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_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_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )

let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds
( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )

let f2 be BinOp of D2; :: thesis: ( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
thus ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 implies [a1,a2] is_a_left_unity_wrt |:f1,f2:| ) :: thesis: ( [a1,a2] is_a_left_unity_wrt |:f1,f2:| implies ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) )
proof
defpred S1[ set ] means |:f1,f2:| . ([a1,a2],\$1) = \$1;
assume A1: for b1 being Element of D1 holds f1 . (a1,b1) = b1 ; :: according to BINOP_1:def 16 :: thesis: ( not a2 is_a_left_unity_wrt f2 or [a1,a2] is_a_left_unity_wrt |:f1,f2:| )
assume A2: for b2 being Element of D2 holds f2 . (a2,b2) = b2 ; :: according to BINOP_1:def 16 :: thesis: [a1,a2] is_a_left_unity_wrt |:f1,f2:|
A3: now :: thesis: for b1 being Element of D1
for b2 being Element of D2 holds S1[[b1,b2]]
let b1 be Element of D1; :: thesis: for b2 being Element of D2 holds S1[[b1,b2]]
let b2 be Element of D2; :: thesis: S1[[b1,b2]]
|:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))] by Th21
.= [b1,(f2 . (a2,b2))] by A1
.= [b1,b2] by A2 ;
hence S1[[b1,b2]] ; :: thesis: verum
end;
thus for a being Element of [:D1,D2:] holds S1[a] from :: according to BINOP_1:def 16 :: thesis: verum
end;
assume A4: for a being Element of [:D1,D2:] holds |:f1,f2:| . ([a1,a2],a) = a ; :: according to BINOP_1:def 16 :: thesis: ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 )
thus for b1 being Element of D1 holds f1 . (a1,b1) = b1 :: according to BINOP_1:def 16 :: thesis:
proof
let b1 be Element of D1; :: thesis: f1 . (a1,b1) = b1
set b2 = the Element of D2;
[(f1 . (a1,b1)),(f2 . (a2, the Element of D2))] = |:f1,f2:| . ([a1,a2],[b1, the Element of D2]) by Th21
.= [b1, the Element of D2] by A4 ;
hence f1 . (a1,b1) = b1 by XTUPLE_0:1; :: thesis: verum
end;
set b1 = the Element of D1;
let b2 be Element of D2; :: according to BINOP_1:def 16 :: thesis: f2 . (a2,b2) = b2
[(f1 . (a1, the Element of D1)),(f2 . (a2,b2))] = |:f1,f2:| . ([a1,a2],[ the Element of D1,b2]) by Th21
.= [ the Element of D1,b2] by A4 ;
hence f2 . (a2,b2) = b2 by XTUPLE_0:1; :: thesis: verum