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