let t1, t2 be finite DecoratedTree of QC-WFF A; :: thesis: ( t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) implies t1 = t2 )
A7: for t1, t2 being finite DecoratedTree of QC-WFF A st t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) holds
t1 c= t2
proof
let t1, t2 be finite DecoratedTree of QC-WFF A; :: thesis: ( t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) implies t1 c= t2 )
assume that
A8: t1 . {} = p and
A9: for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) and
A10: t2 . {} = p and
A11: for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ; :: thesis: t1 c= t2
defpred S1[ set ] means ( $1 in dom t2 & t1 . $1 = t2 . $1 );
A12: for t being Element of dom t1
for n being Nat st S1[t] & t ^ <*n*> in dom t1 holds
S1[t ^ <*n*>]
proof
let t be Element of dom t1; :: thesis: for n being Nat st S1[t] & t ^ <*n*> in dom t1 holds
S1[t ^ <*n*>]
let n be Nat; :: thesis: ( S1[t] & t ^ <*n*> in dom t1 implies S1[t ^ <*n*>] )
assume that
A13: S1[t] and
A14: t ^ <*n*> in dom t1 ; :: thesis: S1[t ^ <*n*>]
reconsider t9 = t as Element of dom t2 by A13;
A15: succ (t1,t) = list_of_immediate_constituents (t2 . t9) by A9, A13
.= succ (t2,t9) by A11 ;
t ^ <*n*> in succ t by A14;
then n < card (succ t) by TREES_9:7;
then n < len (t succ) by TREES_9:def 5;
then n < len (succ (t1,t)) by TREES_9:28;
then n < len (t9 succ) by A15, TREES_9:28;
then n < card (succ t9) by TREES_9:def 5;
then A16: t9 ^ <*n*> in succ t9 by TREES_9:7;
hence t ^ <*n*> in dom t2 ; :: thesis: t1 . (t ^ <*n*>) = t2 . (t ^ <*n*>)
thus t1 . (t ^ <*n*>) = (succ (t2,t9)) . (n + 1) by A14, A15, TREES_9:40
.= t2 . (t ^ <*n*>) by A16, TREES_9:40 ; :: thesis: verum
end;
A17: S1[ {} ] by A8, A10, TREES_1:22;
A18: for t being Element of dom t1 holds S1[t] from TREES_2:sch 1(A17, A12);
 then for t being object st t in dom t1 holds
t in dom t2 ;
then A19: dom t1 c= dom t2 ;
for x being object st x in dom t1 holds
t1 . x = t2 . x by A18;
hence t1 c= t2 by A19, GRFUNC_1:2; :: thesis: verum
end;
assume ( t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) ) ; :: thesis: t1 = t2
then ( t1 c= t2 & t2 c= t1 ) by A7;
hence t1 = t2 ; :: thesis: verum