let S be non empty non void ManySortedSign ; :: thesis: for V1, V2 being V5 ManySortedSet of the carrier of S st V1 c= V2 holds
for t being Term of S,V1 holds t is Term of S,V2
let V1, V2 be V5 ManySortedSet of the carrier of S; :: thesis: ( V1 c= V2 implies for t being Term of S,V1 holds t is Term of S,V2 )
assume A1: for s being set st s in the carrier of S holds
V1 . s c= V2 . s ; :: according to PBOOLE:def 5 :: thesis: for t being Term of S,V1 holds t is Term of S,V2
defpred S₁[ set ] means $1 is Term of S,V2;
A2: for s being SortSymbol of S
for v being Element of V1 . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of S; :: thesis: for v being Element of V1 . s holds S₁[ root-tree [v,s]]
let v be Element of V1 . s; :: thesis: S₁[ root-tree [v,s]]
V1 . s c= V2 . s by A1;
then v in V2 . s by TARSKI:def 3;
hence root-tree [v,s] is Term of S,V2 by Th4; :: thesis: verum

end;

A3: for o being OperSymbol of S
for p being ArgumentSeq of Sym o,V1 st ( for t being Term of S,V1 st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]

proof

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym o,V1 st ( for t being Term of S,V1 st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]
let p be ArgumentSeq of Sym o,V1; :: thesis: ( ( for t being Term of S,V1 st t in rng p holds
S₁[t] ) implies S₁[[o,the carrier of S] -tree p] )
assume A4: for t being Term of S,V1 st t in rng p holds
t is Term of S,V2 ; :: thesis: S₁[[o,the carrier of S] -tree p]
rng p c= S -Terms V2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in S -Terms V2 )
assume A5: x in rng p ; :: thesis: x in S -Terms V2
rng p c= S -Terms V1 by FINSEQ_1:def 4;
then reconsider x = x as Term of S,V1 by A5;
x is Term of S,V2 by A4, A5;
hence x in S -Terms V2 ; :: thesis: verum

end;

then reconsider q = p as FinSequence of S -Terms V2 by FINSEQ_1:def 4;
A6: len p = len (the_arity_of o) by Lm8;

now

let i be Nat; :: thesis: ( i in dom q implies ex T being Term of S,V2 st
( T = q . i & the_sort_of T = (the_arity_of o) . i ) )
assume A7: i in dom q ; :: thesis: ex T being Term of S,V2 st
( T = q . i & the_sort_of T = (the_arity_of o) . i )
then consider t being Term of S,V1 such that
A8: ( t = q . i & t = p /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) by Lm8;
t in rng p by A7, A8, FUNCT_1:def 5;
then reconsider T = t as Term of S,V2 by A4;
take T = T; :: thesis: ( T = q . i & the_sort_of T = (the_arity_of o) . i )
thus T = q . i by A8; :: thesis: the_sort_of T = (the_arity_of o) . i
thus the_sort_of T = (the_arity_of o) . i :: thesis: verum

proof

per cases ( ex s being SortSymbol of S ex v being Element of V1 . s st t . {} = [v,s] or t . {} in [:the carrier' of S,{the carrier of S}:] ) by Th2;

suppose ex s being SortSymbol of S ex v being Element of V1 . s st t . {} = [v,s] ; :: thesis: the_sort_of T = (the_arity_of o) . i

then consider s being SortSymbol of S, v being Element of V1 . s such that
A9: t . {} = [v,s] ;
V1 . s c= V2 . s by A1;
then A10: ( t = root-tree [v,s] & v in V2 . s ) by A9, Th5, TARSKI:def 3;
hence the_sort_of T = s by Th14
.= (the_arity_of o) . i by A8, A10, Th14 ;
:: thesis: verum

end;

suppose t . {} in [:the carrier' of S,{the carrier of S}:] ; :: thesis: the_sort_of T = (the_arity_of o) . i

then consider o' being OperSymbol of S, x2 being Element of {the carrier of S} such that
A11: t . {} = [o',x2] by DOMAIN_1:9;
A12: x2 = the carrier of S by TARSKI:def 1;
hence the_sort_of T = the_result_sort_of o' by A11, Th17
.= (the_arity_of o) . i by A8, A11, A12, Th17 ;
:: thesis: verum

end;

end;

end;

end;

then q is ArgumentSeq of Sym o,V2 by A6, Th24;
hence [o,the carrier of S] -tree p is Term of S,V2 by Th1; :: thesis: verum

end;

for t being Term of S,V1 holds S₁[t] from MSATERM:sch 1(A2, A3);
hence for t being Term of S,V1 holds t is Term of S,V2 ; :: thesis: verum