let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
for o being OperSymbol of S
for x being set st x in (((ParsedTerms X) # ) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
let X be V5() ManySortedSet of ; :: thesis: for o being OperSymbol of S
for x being set st x in (((ParsedTerms X) # ) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
let o be OperSymbol of S; :: thesis: for x being set st x in (((ParsedTerms X) # ) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
let x be set ; :: thesis: ( x in (((ParsedTerms X) # ) * the Arity of S) . o implies x is FinSequence of TS (DTConOSA X) )
assume A1:
x in (((ParsedTerms X) # ) * the Arity of S) . o
; :: thesis: x is FinSequence of TS (DTConOSA X)
set D = DTConOSA X;
set ar = the_arity_of o;
the Arity of S . o = the_arity_of o
by MSUALG_1:def 6;
then
x in product ((ParsedTerms X) * (the_arity_of o))
by A1, MSAFREE:1;
then consider f being Function such that
A2:
( x = f & dom f = dom ((ParsedTerms X) * (the_arity_of o)) & ( for y being set st y in dom ((ParsedTerms X) * (the_arity_of o)) holds
f . y in ((ParsedTerms X) * (the_arity_of o)) . y ) )
by CARD_3:def 5;
A3:
dom ((ParsedTerms X) * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 4;
dom (the_arity_of o) = Seg (len (the_arity_of o))
by FINSEQ_1:def 3;
then reconsider f = f as FinSequence by A2, A3, FINSEQ_1:def 2;
rng f c= TS (DTConOSA X)
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in TS (DTConOSA X) )
assume
a in rng f
;
:: thesis: a in TS (DTConOSA X)
then consider b being
set such that A4:
(
b in dom f &
f . b = a )
by FUNCT_1:def 5;
A5:
a in ((ParsedTerms X) * (the_arity_of o)) . b
by A2, A4;
reconsider b =
b as
Nat by A4;
((ParsedTerms X) * (the_arity_of o)) . b =
(ParsedTerms X) . ((the_arity_of o) . b)
by A2, A4, FUNCT_1:22
.=
(ParsedTerms X) . ((the_arity_of o) /. b)
by A2, A3, A4, PARTFUN1:def 8
.=
ParsedTerms X,
((the_arity_of o) /. b)
by Def8
.=
{ s where s is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= (the_arity_of o) /. b & x in X . s1 & s = root-tree [x,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = s . {} & the_result_sort_of o1 <= (the_arity_of o) /. b ) ) }
;
then consider e being
Element of
TS (DTConOSA X) such that A6:
a = e
and
( ex
s1 being
Element of
S ex
x being
set st
(
s1 <= (the_arity_of o) /. b &
x in X . s1 &
e = root-tree [x,s1] ) or ex
o being
OperSymbol of
S st
(
[o,the carrier of S] = e . {} &
the_result_sort_of o <= (the_arity_of o) /. b ) )
by A5;
thus
a in TS (DTConOSA X)
by A6;
:: thesis: verum
end;
then reconsider f = f as FinSequence of TS (DTConOSA X) by FINSEQ_1:def 4;
f = x
by A2;
hence
x is FinSequence of TS (DTConOSA X)
; :: thesis: verum