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:] & X1 c= D1 & X2 c= D2 ) by Th45;
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 set ; :: 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 set such that
A2: ( y in dom f & y in [:X1,X2:] & x = f . y ) by A1, FUNCT_1:def 12;
consider y1, y2 being set such that
A3: ( y1 in X1 & y2 in X2 & y = [y1,y2] ) by A2, ZFMISC_1:103;
reconsider y1 = y1 as Element of D1 by A3;
reconsider y2 = y2 as Element of D2 by A3;
x = f . y1,y2 by A2, A3;
hence x in { (f . a,b) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) } by A3; :: thesis: verum

end;

let x be set ; :: 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 Th46; :: thesis: verum