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
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; 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; 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; 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 ; ( x1 in X1 & x2 in X2 implies f . (x1,x2) in (f .:^2) . (X1,X2) )
assume that
A1:
x1 in X1
and
A2:
x2 in X2
; f . (x1,x2) in (f .:^2) . (X1,X2)
reconsider b = x2 as Element of D2 by A2;
reconsider a = x1 as Element of D1 by A1;
A3:
( (f .:^2) . (X1,X2) = f .: [:X1,X2:] & dom f = [:D1,D2:] )
by Th44, FUNCT_2:def 1;
[a,b] in [:X1,X2:]
by A1, A2, ZFMISC_1:87;
hence
f . (x1,x2) in (f .:^2) . (X1,X2)
by A3, FUNCT_1:def 6; verum