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, Th6;
consider phi being Function of A,B such that
A4: for x being set st x in dom f9 holds
phi . x = f9 . x by FUNCT_2:136;
reconsider phi = phi as Element of Funcs A,B by FUNCT_2:11;
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:68; :: thesis: verum