let D1, D2 be non empty set ; :: thesis: for a1, b1 being Element of D1

for a2, b2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let a1, b1 be Element of D1; :: thesis: for a2, b2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let a2, b2 be Element of D2; :: thesis: for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let f2 be BinOp of D2; :: thesis: |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

A1: dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by FUNCT_2:def 1;

[[a1,a2],[b1,b2]] in [:[:D1,D2:],[:D1,D2:]:] ;

hence |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))] by A1, FUNCT_4:55; :: thesis: verum

for a2, b2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let a1, b1 be Element of D1; :: thesis: for a2, b2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let a2, b2 be Element of D2; :: thesis: for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let f1 be BinOp of D1; :: thesis: for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

let f2 be BinOp of D2; :: thesis: |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

A1: dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] by FUNCT_2:def 1;

[[a1,a2],[b1,b2]] in [:[:D1,D2:],[:D1,D2:]:] ;

hence |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))] by A1, FUNCT_4:55; :: thesis: verum