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)

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

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 . (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) )
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;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

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