let F be Element of QC-WFF ; :: thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t is_a_proper_prefix_of t9 implies len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume A1: t is_a_proper_prefix_of t9 ; :: thesis: len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
then A2: t is_a_prefix_of t9 by XBOOLE_0:def 8;

A3: now

consider r being FinSequence such that
A4: t9 = t ^ r by A2, TREES_1:1;
reconsider r = r as FinSequence of NAT by A4, FINSEQ_1:36;
A5: 1 <= len r

proof

reconsider t1 = {} as Element of dom (tree_of_subformulae F) by TREES_1:22;
( r <> {} & t1 is_a_prefix_of r ) by A1, A4, FINSEQ_1:34, XBOOLE_1:2;
then A6: t1 is_a_proper_prefix_of r by XBOOLE_0:def 8;
len t1 = 0 ;
then 0 < len r by A6, TREES_1:6;
then 0 + 1 <= len r by NAT_1:13;
hence 1 <= len r ; :: thesis: verum

end;

defpred S₁[ set , set ] means ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = $1 & r1 = r | (Seg m) & t1 = t ^ r1 & $2 = (tree_of_subformulae F) . t1 );
A7: for k being Nat st k in Seg (len r) holds
ex x being set st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len r) implies ex x being set st S₁[k,x] )
assume A8: k in Seg (len r) ; :: thesis: ex x being set st S₁[k,x]
r | (Seg k) is FinSequence by FINSEQ_1:15;
then consider r1 being FinSequence such that
A9: r1 = r | (Seg k) ;
r1 is_a_prefix_of r by A8, A9, TREES_1:def 1;
then t ^ r1 in dom (tree_of_subformulae F) by A4, FINSEQ_6:13, TREES_1:20;
then consider t1 being Element of dom (tree_of_subformulae F) such that
A10: t1 = t ^ r1 ;
ex x being set st x = (tree_of_subformulae F) . t1 ;
hence ex x being set st S₁[k,x] by A9, A10; :: thesis: verum

end;

ex L being FinSequence st
( dom L = Seg (len r) & ( for k being Nat st k in Seg (len r) holds
S₁[k,L . k] ) ) from FINSEQ_1:sch 1(A7);
then consider L being FinSequence such that
dom L = Seg (len r) and
A11: for k being Nat st k in Seg (len r) holds
ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ;
for k being Element of NAT st 1 <= k & k <= len r holds
ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 )

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= len r implies ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) )
assume ( 1 <= k & k <= len r ) ; :: thesis: ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 )
then k in Seg (len r) by FINSEQ_1:1;
then ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) by A11;
hence ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ; :: thesis: verum

end;

then consider t1 being Element of dom (tree_of_subformulae F), r1 being FinSequence such that
A12: r1 = r | (Seg 1) and
A13: t1 = t ^ r1 and
L . 1 = (tree_of_subformulae F) . t1 by A5;
set H1 = (tree_of_subformulae F) . t1;
A14: (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t

proof

ex m being Element of NAT st r1 = <*m*> by A5, A12, TREES_9:34;
hence (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t by A13, Th36; :: thesis: verum

end;

r1 is_a_prefix_of r by A12, TREES_1:def 1;
then t1 is_a_prefix_of t9 by A4, A13, FINSEQ_6:13;
then A15: len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t1)) by Th28, Th42;
assume len (@ ((tree_of_subformulae F) . t9)) = len (@ ((tree_of_subformulae F) . t)) ; :: thesis: contradiction
hence contradiction by A15, A14, QC_LANG2:51; :: thesis: verum

end;

len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t)) by A2, Th28, Th42;
hence len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) by A3, XXREAL_0:1; :: thesis: verum