let D1, D2, D be non empty set ; 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; 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; 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; (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 ) }
XBOOLE_0:def 10 { (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 ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( 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 ) }
; 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; verum