let B be non empty set ; :: thesis: for A, X, Y being set st Funcs (X,Y) <> {} & X c= A & Y c= B holds

for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f

let A be set ; :: thesis: for X, Y being set st Funcs (X,Y) <> {} & X c= A & Y c= B holds

for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f

let X, Y be set ; :: thesis: ( Funcs (X,Y) <> {} & X c= A & Y c= B implies for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f )

assume that

A1: Funcs (X,Y) <> {} and

A2: X c= A and

A3: Y c= B ; :: thesis: for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f

let f be Element of Funcs (X,Y); :: thesis: ex phi being Element of Funcs (A,B) st phi | X = f

reconsider f9 = f as PartFunc of A,B by A1, A2, A3, Th3;

consider phi being Function of A,B such that

A4: for x being object st x in dom f9 holds

phi . x = f9 . x by FUNCT_2:71;

reconsider phi = phi as Element of Funcs (A,B) by FUNCT_2:8;

take phi ; :: thesis: phi | X = f

ex g being Function st

( f = g & dom g = X & rng g c= Y ) by A1, FUNCT_2:def 2;

then dom f9 = A /\ X by XBOOLE_1:28

.= (dom phi) /\ X by FUNCT_2:def 1 ;

hence phi | X = f by A4, FUNCT_1:46; :: thesis: verum

for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f

let A be set ; :: thesis: for X, Y being set st Funcs (X,Y) <> {} & X c= A & Y c= B holds

for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f

let X, Y be set ; :: thesis: ( Funcs (X,Y) <> {} & X c= A & Y c= B implies for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f )

assume that

A1: Funcs (X,Y) <> {} and

A2: X c= A and

A3: Y c= B ; :: thesis: for f being Element of Funcs (X,Y) ex phi being Element of Funcs (A,B) st phi | X = f

let f be Element of Funcs (X,Y); :: thesis: ex phi being Element of Funcs (A,B) st phi | X = f

reconsider f9 = f as PartFunc of A,B by A1, A2, A3, Th3;

consider phi being Function of A,B such that

A4: for x being object st x in dom f9 holds

phi . x = f9 . x by FUNCT_2:71;

reconsider phi = phi as Element of Funcs (A,B) by FUNCT_2:8;

take phi ; :: thesis: phi | X = f

ex g being Function st

( f = g & dom g = X & rng g c= Y ) by A1, FUNCT_2:def 2;

then dom f9 = A /\ X by XBOOLE_1:28

.= (dom phi) /\ X by FUNCT_2:def 1 ;

hence phi | X = f by A4, FUNCT_1:46; :: thesis: verum