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

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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum