let P, Q be PNPair; :: thesis: for T being pnptree of P st Q in rng T holds
rng Q c= union (Subt (rng P))
let T be pnptree of P; :: thesis: ( Q in rng T implies rng Q c= union (Subt (rng P)) )
deffunc H₃( PNPair) -> set = { (Sub . A) where A is Element of LTLB_WFF : A in rng $1 } ;
defpred S₁[ set ] means for Q being PNPair st Q = T . $1 & $1 in dom T holds
rng Q c= union (Subt (rng P));
assume Q in rng T ; :: thesis: rng Q c= union (Subt (rng P))
then consider x being object such that
A1: x in dom T and
A2: T . x = Q by FUNCT_1:def 3;
reconsider x = x as Element of dom T by A1;

A3: now :: thesis: for t being Element of dom T
for n being Nat st S₁[t] & t ^ <*n*> in dom T holds
S₁[t ^ <*n*>]

let t be Element of dom T; :: thesis: for n being Nat st S₁[t] & t ^ <*n*> in dom T holds
S₁[t ^ <*n*>]
let n be Nat; :: thesis: ( S₁[t] & t ^ <*n*> in dom T implies S₁[t ^ <*n*>] )
assume that
A4: S₁[t] and
t ^ <*n*> in dom T ; :: thesis: S₁[t ^ <*n*>]
A5: rng (T . t) c= union (Subt (rng P)) by A4;
thus S₁[t ^ <*n*>] :: thesis: verum

proof

let Q be PNPair; :: thesis: ( Q = T . (t ^ <*n*>) & t ^ <*n*> in dom T implies rng Q c= union (Subt (rng P)) )
assume ( Q = T . (t ^ <*n*>) & t ^ <*n*> in dom T ) ; :: thesis: rng Q c= union (Subt (rng P))
then Q in compn (T . t) by Th26;
hence rng Q c= union (Subt (rng P)) by Th23, A5; :: thesis: verum

end;

end;

A6: S₁[ {} ]

proof

let Q be PNPair; :: thesis: ( Q = T . {} & {} in dom T implies rng Q c= union (Subt (rng P)) )
assume that
A7: Q = T . {} and
{} in dom T ; :: thesis: rng Q c= union (Subt (rng P))
Q = P by A7, Def11;
hence rng Q c= union (Subt (rng P)) by Th9; :: thesis: verum

end;

for t being Element of dom T holds S₁[t] from TREES_2:sch 1(A6, A3);
then rng (T . x) c= union (Subt (rng P)) ;
hence rng Q c= union (Subt (rng P)) by A2; :: thesis: verum