let y be Element of rng T; :: thesis: y is complete
defpred S₁[ set ] means for Q being PNPair st Q = T . P & P in dom T holds
Q is complete ;
A1: ex x being object st
( x in dom T & T . x = y ) by FUNCT_1:def 3;

A2: 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
A3: S₁[t] and
t ^ <*n*> in dom T ; :: thesis: S₁[t ^ <*n*>]
reconsider Tt = T . t as Element of rng T by FUNCT_1:def 3;
reconsider pQ = Tt as consistent complete PNPair by A3;
thus S₁[t ^ <*n*>] :: thesis: verum

proof

let Q be PNPair; :: thesis: ( Q = T . (t ^ <*n*>) & t ^ <*n*> in dom T implies Q is complete )
assume ( Q = T . (t ^ <*n*>) & t ^ <*n*> in dom T ) ; :: thesis: Q is complete
then reconsider Q1 = Q as Element of compn pQ by Th26;
Q1 is consistent ;
hence Q is complete ; :: thesis: verum

end;

end;

A4: S₁[ {} ] by Def11;
for t being Element of dom T holds S₁[t] from TREES_2:sch 1(A4, A2);
hence y is complete by A1; :: thesis: verum