let S be non empty non void ManySortedSign ; :: thesis: for V1, V2 being V2() 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 V2() 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 object st s in the carrier of S holds
V1 . s c= V2 . s ; :: according to PBOOLE:def 2 :: thesis: for t being Term of S,V1 holds t is Term of S,V2
defpred S1[ set ] means $1 is Term of S,V2;
A2: 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
S1[t] ) holds
S1[[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
S1[t] ) holds
S1[[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
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A3: for t being Term of S,V1 st t in rng p holds
t is Term of S,V2 ; :: thesis: S1[[o, the carrier of S] -tree p]
rng p c= S -Terms V2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in S -Terms V2 )
assume A4: 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 A4;
x is Term of S,V2 by A3, A4;
hence x in S -Terms V2 ; :: thesis: verum
end;
then reconsider q = p as FinSequence of S -Terms V2 by FINSEQ_1:def 4;
A5: now :: thesis: for i being Nat st i in dom q holds
ex T being Term of S,V2 st
( T = q . i & the_sort_of T = (the_arity_of o) . i )
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 A6: 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
A7: t = q . i and
t = p /. i and
A8: the_sort_of t = (the_arity_of o) . i and
the_sort_of t = (the_arity_of o) /. i by Lm8;
t in rng p by A6, A7, FUNCT_1:def 3;
then reconsider T = t as Term of S,V2 by A3;
take T = T; :: thesis: ( T = q . i & the_sort_of T = (the_arity_of o) . i )
thus T = q . i by A7; :: 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] ;
A10: t = root-tree [v,s] by A9, Th5;
V1 . s c= V2 . s by A1;
then v in V2 . s ;
hence the_sort_of T = s by A10, 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 o9 being OperSymbol of S, x2 being Element of { the carrier of S} such that
A11: t . {} = [o9,x2] by DOMAIN_1:1;
A12: x2 = the carrier of S by TARSKI:def 1;
hence the_sort_of T = the_result_sort_of o9 by A11, Th17
.= (the_arity_of o) . i by A8, A11, A12, Th17 ;
:: thesis: verum
end;
end;
end;
end;
len p = len (the_arity_of o) by Lm8;
then q is ArgumentSeq of Sym (o,V2) by A5, Th24;
hence S1[[o, the carrier of S] -tree p] by Th1; :: thesis: verum
end;
A13: for s being SortSymbol of S
for v being Element of V1 . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; :: thesis: for v being Element of V1 . s holds S1[ root-tree [v,s]]
let v be Element of V1 . s; :: thesis: S1[ root-tree [v,s]]
V1 . s c= V2 . s by A1;
then v in V2 . s ;
hence S1[ root-tree [v,s]] by Th4; :: thesis: verum
end;
for t being Term of S,V1 holds S1[t] from MSATERM:sch 1(A13, A2);
 hence for t being Term of S,V1 holds t is Term of S,V2 ; :: thesis: verum