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_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_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_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_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_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds

( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

let f2 be BinOp of D2; :: thesis: ( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

thus ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 implies [a1,a2] is_a_right_unity_wrt |:f1,f2:| ) :: thesis: ( [a1,a2] is_a_right_unity_wrt |:f1,f2:| implies ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) )

thus for b1 being Element of D1 holds f1 . (b1,a1) = b1 :: according to BINOP_1:def 17 :: thesis: a2 is_a_right_unity_wrt f2

let b2 be Element of D2; :: according to BINOP_1:def 17 :: thesis: f2 . (b2,a2) = b2

[(f1 . ( the Element of D1,a1)),(f2 . (b2,a2))] = |:f1,f2:| . ([ the Element of D1,b2],[a1,a2]) by Th21

.= [ the Element of D1,b2] by A4 ;

hence f2 . (b2,a2) = b2 by XTUPLE_0:1; :: thesis: verum

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_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_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_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_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds

( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

let f2 be BinOp of D2; :: thesis: ( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

thus ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 implies [a1,a2] is_a_right_unity_wrt |:f1,f2:| ) :: thesis: ( [a1,a2] is_a_right_unity_wrt |:f1,f2:| implies ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) )

proof

assume A4:
for a being Element of [:D1,D2:] holds |:f1,f2:| . (a,[a1,a2]) = a
; :: according to BINOP_1:def 17 :: thesis: ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 )
defpred S_{1}[ set ] means |:f1,f2:| . ($1,[a1,a2]) = $1;

assume A1: for b1 being Element of D1 holds f1 . (b1,a1) = b1 ; :: according to BINOP_1:def 17 :: thesis: ( not a2 is_a_right_unity_wrt f2 or [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

assume A2: for b2 being Element of D2 holds f2 . (b2,a2) = b2 ; :: according to BINOP_1:def 17 :: thesis: [a1,a2] is_a_right_unity_wrt |:f1,f2:|

_{1}[a]
from FILTER_1:sch 4(A3); :: according to BINOP_1:def 17 :: thesis: verum

end;assume A1: for b1 being Element of D1 holds f1 . (b1,a1) = b1 ; :: according to BINOP_1:def 17 :: thesis: ( not a2 is_a_right_unity_wrt f2 or [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

assume A2: for b2 being Element of D2 holds f2 . (b2,a2) = b2 ; :: according to BINOP_1:def 17 :: thesis: [a1,a2] is_a_right_unity_wrt |:f1,f2:|

A3: now :: thesis: for b1 being Element of D1

for b2 being Element of D2 holds S_{1}[[b1,b2]]

thus
for a being Element of [:D1,D2:] holds Sfor b2 being Element of D2 holds S

let b1 be Element of D1; :: thesis: for b2 being Element of D2 holds S_{1}[[b1,b2]]

let b2 be Element of D2; :: thesis: S_{1}[[b1,b2]]

|:f1,f2:| . ([b1,b2],[a1,a2]) = [(f1 . (b1,a1)),(f2 . (b2,a2))] by Th21

.= [b1,(f2 . (b2,a2))] by A1

.= [b1,b2] by A2 ;

hence S_{1}[[b1,b2]]
; :: thesis: verum

end;let b2 be Element of D2; :: thesis: S

|:f1,f2:| . ([b1,b2],[a1,a2]) = [(f1 . (b1,a1)),(f2 . (b2,a2))] by Th21

.= [b1,(f2 . (b2,a2))] by A1

.= [b1,b2] by A2 ;

hence S

thus for b1 being Element of D1 holds f1 . (b1,a1) = b1 :: according to BINOP_1:def 17 :: thesis: a2 is_a_right_unity_wrt f2

proof

set b1 = the Element of D1;
let b1 be Element of D1; :: thesis: f1 . (b1,a1) = b1

set b2 = the Element of D2;

[(f1 . (b1,a1)),(f2 . ( the Element of D2,a2))] = |:f1,f2:| . ([b1, the Element of D2],[a1,a2]) by Th21

.= [b1, the Element of D2] by A4 ;

hence f1 . (b1,a1) = b1 by XTUPLE_0:1; :: thesis: verum

end;set b2 = the Element of D2;

[(f1 . (b1,a1)),(f2 . ( the Element of D2,a2))] = |:f1,f2:| . ([b1, the Element of D2],[a1,a2]) by Th21

.= [b1, the Element of D2] by A4 ;

hence f1 . (b1,a1) = b1 by XTUPLE_0:1; :: thesis: verum

let b2 be Element of D2; :: according to BINOP_1:def 17 :: thesis: f2 . (b2,a2) = b2

[(f1 . ( the Element of D1,a1)),(f2 . (b2,a2))] = |:f1,f2:| . ([ the Element of D1,b2],[a1,a2]) by Th21

.= [ the Element of D1,b2] by A4 ;

hence f2 . (b2,a2) = b2 by XTUPLE_0:1; :: thesis: verum