let t1, t2 be finite DecoratedTree of QC-WFF ; :: 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 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 ; :: 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 S₁[ set ] means ( $1 in dom t2 & t1 . $1 = t2 . $1 );
A12: for t being Element of dom t1
for n being Element of NAT st S₁[t] & t ^ <*n*> in dom t1 holds
S₁[t ^ <*n*>]

proof

let t be Element of dom t1; :: thesis: for n being Element of NAT st S₁[t] & t ^ <*n*> in dom t1 holds
S₁[t ^ <*n*>]
let n be Element of NAT ; :: thesis: ( S₁[t] & t ^ <*n*> in dom t1 implies S₁[t ^ <*n*>] )
assume that
A13: S₁[t] and
A14: t ^ <*n*> in dom t1 ; :: thesis: S₁[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:29;
then n < len (t9 succ ) by A15, TREES_9:29;
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, Th13
.= t2 . (t ^ <*n*>) by A16, Th13 ; :: thesis: verum

end;

A17: S₁[ {} ] by A8, A10, TREES_1:47;
A18: for t being Element of dom t1 holds S₁[t] from TREES_2:sch 1(A17, A12);
then for t being set st t in dom t1 holds
t in dom t2 ;
then A19: dom t1 c= dom t2 by TARSKI:def 3;
for x being set st x in dom t1 holds
t1 . x = t2 . x by A18;
hence t1 c= t2 by A19, GRFUNC_1:8; :: 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 by XBOOLE_0:def 10; :: thesis: verum