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) holds f is PartFunc of A,B
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) holds f is PartFunc of A,B
let X, Y be set ; :: thesis: ( Funcs (X,Y) <> {} & X c= A & Y c= B implies for f being Element of Funcs (X,Y) holds f is PartFunc of A,B )
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) holds f is PartFunc of A,B
let f be Element of Funcs (X,Y); :: thesis: f is PartFunc of A,B
consider g being Function such that
A4: f = g and
A5: dom g = X and
A6: rng g c= Y by A1, FUNCT_2:def 2;
rng g c= B by A3, A6;
hence f is PartFunc of A,B by A2, A4, A5, RELSET_1:4; :: thesis: verum