let p be FinTree-yielding FinSequence; :: thesis: for n being empty Element of tree p holds card (succ n) = len p
let n be empty Element of tree p; :: thesis: card (succ n) = len p
assume A1: not card (succ n) = len p ; :: thesis: contradiction

per cases ( card (succ n) < len p or card (succ n) > len p ) by A1, XXREAL_0:1;

suppose A2: card (succ n) < len p ; :: thesis: contradiction

then (card (succ n)) + 1 in dom p by Lm3;
then reconsider t = p . ((card (succ n)) + 1) as finite Tree by TREES_3:23;
A3: n ^ <*(card (succ n))*> = <*(card (succ n))*> by FINSEQ_1:34;
( n in t & <*(card (succ n))*> ^ n = <*(card (succ n))*> ) by FINSEQ_1:34, TREES_1:22;
then n ^ <*(card (succ n))*> in tree p by A2, A3, TREES_3:def 15;
then n ^ <*(card (succ n))*> in succ n ;
hence contradiction by Th7; :: thesis: verum

end;

suppose card (succ n) > len p ; :: thesis: contradiction

then n ^ <*(len p)*> in succ n by Th7;
then n ^ <*(len p)*> in tree p ;
then <*(len p)*> in tree p by FINSEQ_1:34;
then consider i being Nat, q being FinSequence such that
A4: i < len p and
q in p . (i + 1) and
A5: <*(len p)*> = <*i*> ^ q by TREES_3:def 15;
len p = <*(len p)*> . 1
.= i by A5, FINSEQ_1:41 ;
hence contradiction by A4; :: thesis: verum

end;

end;