let X, Y be set ; :: thesis: for P being compatible PFUNC_DOMAIN of X,Y holds union P is PartFunc of X,Y
let D be compatible PFUNC_DOMAIN of X,Y; :: thesis: union D is PartFunc of X,Y
set E = { (dom f) where f is Element of D : verum } ;
set F = { (rng f) where f is Element of D : verum } ;
reconsider u = union D as Function ;
A1: rng u c= Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng u or y in Y )
assume y in rng u ; :: thesis: y in Y
then y in union { (rng f) where f is Element of D : verum } by Th13;
then consider Z being set such that
A2: y in Z and
A3: Z in { (rng f) where f is Element of D : verum } by TARSKI:def 4;
consider f being Element of D such that
A4: Z = rng f by A3;
rng f c= Y by RELAT_1:def 19;
hence y in Y by A2, A4; :: thesis: verum

end;

dom u c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom u or x in X )
assume x in dom u ; :: thesis: x in X
then x in union { (dom f) where f is Element of D : verum } by Th11;
then consider Z being set such that
A5: x in Z and
A6: Z in { (dom f) where f is Element of D : verum } by TARSKI:def 4;
ex f being Element of D st Z = dom f by A6;
hence x in X by A5; :: thesis: verum

end;

hence union D is PartFunc of X,Y by A1, RELSET_1:4; :: thesis: verum