let D1, D2 be non empty set ; 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; 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; 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; 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; |: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; verum