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,a2],[b1,b2]] in [:[:D1,D2:],[:D1,D2:]:] & f1 . a1,b1 = f1 . [a1,b1] & f2 . a2,b2 = f2 . [a2,b2] & |:f1,f2:| . [a1,a2],[b1,b2] = |:f1,f2:| . [[a1,a2],[b1,b2]] & dom |:f1,f2:| = [:[:D1,D2:],[:D1,D2:]:] ) by FUNCT_2:def 1;
hence |:f1,f2:| . [a1,a2],[b1,b2] = [(f1 . a1,b1),(f2 . a2,b2)] by FUNCT_4:58; :: thesis: verum