let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t, t1 being Element of (Free (S,X)) st t c= t1 holds
t = t1
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t, t1 being Element of (Free (S,X)) st t c= t1 holds
t = t1
let t, t1 be Element of (Free (S,X)); :: thesis: ( t c= t1 implies t = t1 )
assume A1: t c= t1 ; :: thesis: t = t1
defpred S₁[ Element of (Free (S,X))] means for t1 being Element of (Free (S,X)) st $1 c= t1 holds
$1 = t1;
A2: for s being SortSymbol of S
for x being Element of X . s holds S₁[x -term ]

proof

let s be SortSymbol of S; :: thesis: for x being Element of X . s holds S₁[x -term ]
let x be Element of X . s; :: thesis: S₁[x -term ]
let t1 be Element of (Free (S,X)); :: thesis: ( x -term c= t1 implies x -term = t1 )
assume A3: x -term c= t1 ; :: thesis: x -term = t1
{} in dom (x -term) by TREES_1:22;
then A4: ( t1 . {} = (x -term) . {} & (x -term) . {} = [x,s] ) by A3, GRFUNC_1:2, TREES_4:3;

per cases ( ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p ) by Th16;

suppose ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term ; :: thesis: x -term = t1

then consider s1 being SortSymbol of S, x11 being Element of X . s1 such that
A5: t1 = x11 -term ;
thus x -term = t1 by A5, A4, TREES_4:3; :: thesis: verum

end;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p ; :: thesis: x -term = t1

then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A6: t1 = o -term p ;
t1 . {} = [o, the carrier of S] by A6, TREES_4:def 4;
then ( s in the carrier of S & the carrier of S = s ) by A4, XTUPLE_0:1;
hence x -term = t1 ; :: thesis: verum

end;

end;

end;

A7: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]

proof

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) implies S₁[o -term p] )
assume Z0: for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
let t1 be Element of (Free (S,X)); :: thesis: ( o -term p c= t1 implies o -term p = t1 )
assume Z1: o -term p c= t1 ; :: thesis: o -term p = t1
{} in dom (o -term p) by TREES_1:22;
then A8: ( t1 . {} = (o -term p) . {} & (o -term p) . {} = [o, the carrier of S] ) by Z1, GRFUNC_1:2, TREES_4:def 4;

per cases ( ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p ) by Th16;

suppose ex s being SortSymbol of S ex x being Element of X . s st t1 = x -term ; :: thesis: o -term p = t1

then consider s1 being SortSymbol of S, x11 being Element of X . s1 such that
A5: t1 = x11 -term ;
t1 . {} = [x11,s1] by A5, TREES_4:3;
then ( s1 in the carrier of S & the carrier of S = s1 ) by A8, XTUPLE_0:1;
hence o -term p = t1 ; :: thesis: verum

end;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t1 = o -term p ; :: thesis: o -term p = t1

then consider o1 being OperSymbol of S, p1 being Element of Args (o1,(Free (S,X))) such that
A6: t1 = o1 -term p1 ;
t1 . {} = [o1, the carrier of S] by A6, TREES_4:def 4;
then A7: o = o1 by A8, XTUPLE_0:1;
p = p1

proof

A8: ( dom p = dom (the_arity_of o) & dom (the_arity_of o) = dom p1 ) by A7, MSUALG_6:2;
hence B3: len p = len p1 by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len p or p . b₁ = p1 . b₁ )
let i be Nat; :: thesis: ( not 1 <= i or not i <= len p or p . i = p1 . i )
assume A9: ( 1 <= i & i <= len p ) ; :: thesis: p . i = p1 . i
then B8: i in dom p by FINSEQ_3:25;
reconsider t = p . i, t1 = p1 . i as Element of (Free (S,X)) by A8, A9, FUNCT_1:102, FINSEQ_3:25;
consider j being Nat such that
B2: i = 1 + j by A9, NAT_1:10;
B7: j < len p by A9, B2, NAT_1:13;
then B4: ( t = (o -term p) | <*j*> & t1 = (o1 -term p1) | <*j*> ) by B2, B3, TREES_4:def 4;
then B5: ( dom t = (dom (o -term p)) | <*j*> & dom t1 = (dom (o1 -term p1)) | <*j*> ) by TREES_2:def 10;
(doms p) . (j + 1) = dom t by B2, B8, FUNCT_6:def 2;
then ( {} in (doms p) . (j + 1) & dom (o -term p) = tree (doms p) & len (doms p) = len p ) by TREES_3:38, TREES_4:10, TREES_1:22;
then B6: <*j*> ^ {} in dom (o -term p) by B7, TREES_3:48;
(doms p1) . (j + 1) = dom t1 by B2, A9, A8, FINSEQ_3:25, FUNCT_6:def 2;
then ( {} in (doms p1) . (j + 1) & dom (o1 -term p1) = tree (doms p1) & len (doms p1) = len p1 ) by TREES_3:38, TREES_4:10, TREES_1:22;
then BB: <*j*> ^ {} in dom (o1 -term p1) by B3, B7, TREES_3:48;
BE: t c= t1

proof

let a be object ; :: according to RELAT_1:def 3 :: thesis: for b₁ being object holds
( not [a,b₁] in t or [a,b₁] in t1 )
let b be object ; :: thesis: ( not [a,b] in t or [a,b] in t1 )
assume B1: [a,b] in t ; :: thesis: [a,b] in t1
then reconsider a = a as Node of t by XTUPLE_0:def 12;
t . a = b by B1, FUNCT_1:1;
then BA: ( (o -term p) . (<*j*> ^ a) = b & <*j*> ^ a in dom (o -term p) ) by B4, B5, B6, TREES_1:def 6, TREES_2:def 10;
then BC: ( (o1 -term p1) . (<*j*> ^ a) = b & dom (o -term p) c= dom (o1 -term p1) ) by Z1, A6, GRFUNC_1:2;
then BD: a in dom t1 by BA, BB, B5, TREES_1:def 6;
then t1 . a = b by BC, B4, B5, TREES_2:def 10;
hence [a,b] in t1 by BD, FUNCT_1:1; :: thesis: verum

end;

t in rng p by B8, FUNCT_1:def 3;
hence p . i = p1 . i by BE, Z0; :: thesis: verum

end;

hence o -term p = t1 by A6, A8, TREES_4:def 4; :: thesis: verum

end;

end;

end;

S₁[t] from MSAFREE5:sch 2(A2, A7);
hence t = t1 by A1; :: thesis: verum