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 S₁[ 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 S₁[[b1,b2]]

let b1 be Element of D1; :: thesis: for b2 being Element of D2 holds S₁[[b1,b2]]
let b2 be Element of D2; :: thesis: S₁[[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 S₁[[b1,b2]] ; :: thesis: verum

end;

thus for a being Element of [:D1,D2:] holds S₁[a] from FILTER_1:sch 4(A3); :: 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: a2 is_a_left_unity_wrt f2

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