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: dom u c= X

proof

let x be set ; :: 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 Th15;
then consider Z being set such that
A2: ( x in Z & Z in { (dom f) where f is Element of D : verum } ) by TARSKI:def 4;
consider f being Element of D such that
A3: Z = dom f by A2;
thus x in X by A2, A3; :: thesis: verum

end;

rng u c= Y

proof

let y be set ; :: 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 Th17;
then consider Z being set such that
A4: ( y in Z & Z in { (rng f) where f is Element of D : verum } ) by TARSKI:def 4;
consider f being Element of D such that
A5: Z = rng f by A4;
rng f c= Y by RELAT_1:def 19;
hence y in Y by A4, A5; :: thesis: verum

end;

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