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

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:|
defpred S₁[ set ] means |:f1,f2:| . [a1,a2],$1 = $1;

A3: now

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 Th22
.= [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
consider b2 being Element of D2;
[(f1 . a1,b1),(f2 . a2,b2)] = |:f1,f2:| . [a1,a2],[b1,b2] by Th22
.= [b1,b2] by A4 ;
hence f1 . a1,b1 = b1 by ZFMISC_1:33; :: thesis: verum

end;

let b2 be Element of D2; :: according to BINOP_1:def 16 :: thesis: f2 . a2,b2 = b2
consider b1 being Element of D1;
[(f1 . a1,b1),(f2 . a2,b2)] = |:f1,f2:| . [a1,a2],[b1,b2] by Th22
.= [b1,b2] by A4 ;
hence f2 . a2,b2 = b2 by ZFMISC_1:33; :: thesis: verum