let D1, D2, D be non empty set ; :: thesis: for f being Function of [:D1,D2:],D

for X1 being Subset of D1

for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

let f be Function of [:D1,D2:],D; :: thesis: for X1 being Subset of D1

for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

let X1 be Subset of D1; :: thesis: for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

let X2 be Subset of D2; :: thesis: (f .:^2) . (X1,X2) = f .: [:X1,X2:]

( [X1,X2] `1 = X1 & [X1,X2] `2 = X2 ) ;

hence (f .:^2) . (X1,X2) = f .: [:X1,X2:] by Def8; :: thesis: verum

for X1 being Subset of D1

for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

let f be Function of [:D1,D2:],D; :: thesis: for X1 being Subset of D1

for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

let X1 be Subset of D1; :: thesis: for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = f .: [:X1,X2:]

let X2 be Subset of D2; :: thesis: (f .:^2) . (X1,X2) = f .: [:X1,X2:]

( [X1,X2] `1 = X1 & [X1,X2] `2 = X2 ) ;

hence (f .:^2) . (X1,X2) = f .: [:X1,X2:] by Def8; :: thesis: verum