let P be PNPair; :: thesis: for T being pnptree of P
for t being Node of T
for n being Nat st t ^ <*n*> in dom T holds
T . (t ^ <*n*>) in compn (T . t)
let T be pnptree of P; :: thesis: for t being Node of T
for n being Nat st t ^ <*n*> in dom T holds
T . (t ^ <*n*>) in compn (T . t)
let t be Node of T; :: thesis: for n being Nat st t ^ <*n*> in dom T holds
T . (t ^ <*n*>) in compn (T . t)
let n be Nat; :: thesis: ( t ^ <*n*> in dom T implies T . (t ^ <*n*>) in compn (T . t) )
set tn = t ^ <*n*>;
assume A1: t ^ <*n*> in dom T ; :: thesis: T . (t ^ <*n*>) in compn (T . t)
dom (succ (T,t)) = dom (t succ) by TREES_9:38;
then A2: (succ (T,t)) . (n + 1) in rng (succ (T,t)) by TREES_9:39, A1, FUNCT_1:3;
A3: succ (T,t) = the Enumeration of compn (T . t) by Def11;
T . (t ^ <*n*>) = (succ (T,t)) . (n + 1) by A1, TREES_9:40;
hence T . (t ^ <*n*>) in compn (T . t) by A3, A2, RLAFFIN3:def 1; :: thesis: verum