let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
let X be V5() ManySortedSet of the carrier of S; for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
let o be OperSymbol of S; for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
let x be set ; ( x in (((FreeSort X) #) * the Arity of S) . o implies x is FinSequence of TS (DTConMSA X) )
set D = DTConMSA X;
set ar = the_arity_of o;
set cr = the carrier of S;
A1:
the Arity of S . o = the_arity_of o
by MSUALG_1:def 1;
( rng (the_arity_of o) c= the carrier of S & dom (FreeSort X) = the carrier of S )
by FINSEQ_1:def 4, PARTFUN1:def 2;
then A2:
dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
assume
x in (((FreeSort X) #) * the Arity of S) . o
; x is FinSequence of TS (DTConMSA X)
then
x in product ((FreeSort X) * (the_arity_of o))
by A1, Th1;
then consider f being Function such that
A3:
x = f
and
A4:
dom f = dom ((FreeSort X) * (the_arity_of o))
and
A5:
for y being object st y in dom ((FreeSort X) * (the_arity_of o)) holds
f . y in ((FreeSort X) * (the_arity_of o)) . y
by CARD_3:def 5;
dom (the_arity_of o) = Seg (len (the_arity_of o))
by FINSEQ_1:def 3;
then reconsider f = f as FinSequence by A4, A2, FINSEQ_1:def 2;
rng f c= TS (DTConMSA X)
proof
let a be
object ;
TARSKI:def 3 ( not a in rng f or a in TS (DTConMSA X) )
assume
a in rng f
;
a in TS (DTConMSA X)
then consider b being
object such that A6:
b in dom f
and A7:
f . b = a
by FUNCT_1:def 3;
A8:
a in ((FreeSort X) * (the_arity_of o)) . b
by A4, A5, A6, A7;
reconsider b =
b as
Nat by A6;
((FreeSort X) * (the_arity_of o)) . b =
(FreeSort X) . ((the_arity_of o) . b)
by A4, A6, FUNCT_1:12
.=
(FreeSort X) . ((the_arity_of o) /. b)
by A4, A2, A6, PARTFUN1:def 6
.=
FreeSort (
X,
((the_arity_of o) /. b))
by Def11
.=
{ s where s is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . ((the_arity_of o) /. b) & s = root-tree [x,((the_arity_of o) /. b)] ) 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
ex
e being
Element of
TS (DTConMSA X) st
(
a = e & ( ex
x being
set st
(
x in X . ((the_arity_of o) /. b) &
e = root-tree [x,((the_arity_of o) /. b)] ) 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 A8;
hence
a in TS (DTConMSA X)
;
verum
end;
then reconsider f = f as FinSequence of TS (DTConMSA X) by FINSEQ_1:def 4;
f = x
by A3;
hence
x is FinSequence of TS (DTConMSA X)
; verum