let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
let V be V2() ManySortedSet of the carrier of S; :: thesis: for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
set X = V;
let o be OperSymbol of S; :: thesis: for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)
let a be FinSequence; :: thesis: ( ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) implies a is ArgumentSeq of Sym (o,V) )
assume that
A1: ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) and
A2: ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) ; :: thesis: a is ArgumentSeq of Sym (o,V)
rng a c= TS (DTConMSA V)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in TS (DTConMSA V) )
assume x in rng a ; :: thesis: x in TS (DTConMSA V)
then consider i being object such that
A3: i in dom a and
A4: x = a . i by FUNCT_1:def 3;
reconsider i = i as Nat by A3;
( ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) by A2, A3;
hence x in TS (DTConMSA V) by A4; :: thesis: verum
end;
then reconsider p = a as FinSequence of TS (DTConMSA V) by FINSEQ_1:def 4;
A5: dom a = dom (the_arity_of o) by A1, FINSEQ_3:29;
now :: thesis: for n being Nat st n in dom p holds
p . n in FreeSort (V,((the_arity_of o) /. n))
let n be Nat; :: thesis: ( n in dom p implies p . n in FreeSort (V,((the_arity_of o) /. n)) )
assume A6: n in dom p ; :: thesis: p . n in FreeSort (V,((the_arity_of o) /. n))
thus p . n in FreeSort (V,((the_arity_of o) /. n)) :: thesis: verum
proof
per cases ( ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) . n ) or ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ) by A2, A6;
suppose ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) . n ) ; :: thesis: p . n in FreeSort (V,((the_arity_of o) /. n))
then consider t being Term of S,V such that
A7: t = a . n and
A8: the_sort_of t = (the_arity_of o) . n ;
the_sort_of t = (the_arity_of o) /. n by A5, A6, A8, PARTFUN1:def 6;
hence p . n in FreeSort (V,((the_arity_of o) /. n)) by A7, Def5; :: thesis: verum
end;
suppose ex t being Term of S,V st
( t = a . n & the_sort_of t = (the_arity_of o) /. n ) ; :: thesis: p . n in FreeSort (V,((the_arity_of o) /. n))
hence p . n in FreeSort (V,((the_arity_of o) /. n)) by Def5; :: thesis: verum
end;
end;
end;
end;
then p in (((FreeSort V) #) * the Arity of S) . o by A5, MSAFREE:9;
then A9: Sym (o,V) ==> roots p by MSAFREE:10;
S -Terms V = TS (DTConMSA V) ;
hence a is ArgumentSeq of Sym (o,V) by A9, Th21; :: thesis: verum