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