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:58; :: thesis: verum