let X, Y be set ; :: thesis: for B being c=-linear Subset of (PFuncs X,Y) holds union B in PFuncs X,Y
let B be c=-linear Subset of (PFuncs X,Y); :: thesis: union B in PFuncs X,Y
for x being set st x in B holds
x is Function ;
then reconsider f = union B as Function by TREES_2:36;

per cases ( B <> {} or B = {} ) ;

suppose B <> {} ; :: thesis: union B in PFuncs X,Y

then reconsider D = B as functional non empty set ;

A1: now

let x be set ; :: thesis: ( x in { (dom g) where g is Element of D : verum } implies x c= X )
assume x in { (dom g) where g is Element of D : verum } ; :: thesis: x c= X
then consider g being Element of D such that
A2: x = dom g ;
g in PFuncs X,Y by TARSKI:def 3;
then ex f being Function st
( g = f & dom f c= X & rng f c= Y ) by PARTFUN1:def 5;
hence x c= X by A2; :: thesis: verum

end;

A3: now

let x be set ; :: thesis: ( x in { (rng g) where g is Element of D : verum } implies x c= Y )
assume x in { (rng g) where g is Element of D : verum } ; :: thesis: x c= Y
then consider g being Element of D such that
A4: x = rng g ;
g in PFuncs X,Y by TARSKI:def 3;
then ex f being Function st
( g = f & dom f c= X & rng f c= Y ) by PARTFUN1:def 5;
hence x c= Y by A4; :: thesis: verum

end;

( dom f = union { (dom g) where g is Element of D : verum } & rng f = union { (rng g) where g is Element of D : verum } ) by Th5;
then ( dom f c= X & rng f c= Y ) by A1, A3, ZFMISC_1:94;
hence union B in PFuncs X,Y by PARTFUN1:def 5; :: thesis: verum

end;

suppose A5: B = {} ; :: thesis: union B in PFuncs X,Y

{} is PartFunc of X,Y by RELSET_1:25;
hence union B in PFuncs X,Y by A5, PARTFUN1:119, ZFMISC_1:2; :: thesis: verum

end;

end;