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
for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . x1,x2 in (f .:^2 ) . X1,X2
let f be Function of D1,D2,D; :: thesis: for X1 being Subset of D1
for X2 being Subset of D2
for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . x1,x2 in (f .:^2 ) . X1,X2
let X1 be Subset of D1; :: thesis: for X2 being Subset of D2
for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . x1,x2 in (f .:^2 ) . X1,X2
let X2 be Subset of D2; :: thesis: for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . x1,x2 in (f .:^2 ) . X1,X2
let x1, x2 be set ; :: thesis: ( x1 in X1 & x2 in X2 implies f . x1,x2 in (f .:^2 ) . X1,X2 )
assume A1: ( x1 in X1 & x2 in X2 ) ; :: thesis: f . x1,x2 in (f .:^2 ) . X1,X2
then reconsider a = x1 as Element of D1 ;
reconsider b = x2 as Element of D2 by A1;
A2: (f .:^2 ) . X1,X2 = f .: [:X1,X2:] by Th45;
( f . a,b = f . [a,b] & [a,b] in [:X1,X2:] & dom f = [:D1,D2:] ) by A1, FUNCT_2:def 1, ZFMISC_1:106;
hence f . x1,x2 in (f .:^2 ) . X1,X2 by A2, FUNCT_1:def 12; :: thesis: verum