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 . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in 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 . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) }
let X1 be Subset of D1; :: thesis: for X2 being Subset of D2 holds (f .:^2) . (X1,X2) = { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) }
let X2 be Subset of D2; :: thesis: (f .:^2) . (X1,X2) = { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) }
set A = { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } ;
A1: (f .:^2) . (X1,X2) = f .: [:X1,X2:] by Th44;
thus (f .:^2) . (X1,X2) c= { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } :: according to XBOOLE_0:def 10 :: thesis: { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } c= (f .:^2) . (X1,X2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f .:^2) . (X1,X2) or x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } )
assume x in (f .:^2) . (X1,X2) ; :: thesis: x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) }
then consider y being object such that
y in dom f and
A2: y in [:X1,X2:] and
A3: x = f . y by A1, FUNCT_1:def 6;
consider y1, y2 being object such that
A4: y1 in X1 and
A5: y2 in X2 and
A6: y = [y1,y2] by A2, ZFMISC_1:84;
reconsider y2 = y2 as Element of D2 by A5;
reconsider y1 = y1 as Element of D1 by A4;
x = f . (y1,y2) by A3, A6;
hence x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } by A4, A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } or x in (f .:^2) . (X1,X2) )
assume x in { (f . (a,b)) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } ; :: thesis: x in (f .:^2) . (X1,X2)
then ex a being Element of D1 ex b being Element of D2 st
( x = f . (a,b) & a in X1 & b in X2 ) ;
hence x in (f .:^2) . (X1,X2) by Th45; :: thesis: verum