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, XBOOLE_1:1;
hence f is PartFunc of A,B by A2, A4, A5, RELSET_1:11; :: thesis: verum