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

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