let S be non empty non void ManySortedSign ; for Y being V6() ManySortedSet of the carrier of S
for X, o being set
for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & o -tree p in X holds
p is FinSequence of X
let Y be V6() ManySortedSet of the carrier of S; for X, o being set
for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & o -tree p in X holds
p is FinSequence of X
let X, o be set ; for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & o -tree p in X holds
p is FinSequence of X
let p be DTree-yielding FinSequence; ( ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & o -tree p in X implies p is FinSequence of X )
given C being initialized ConstructorSignature such that A1:
X = Union the Sorts of (Free (S,Y))
; ( not o -tree p in X or p is FinSequence of X )
assume
o -tree p in X
; p is FinSequence of X
then reconsider e = o -tree p as Element of (Free (S,Y)) by A1;
rng p c= X
proof
let z be
object ;
TARSKI:def 3 ( not z in rng p or z in X )
assume
z in rng p
;
z in X
then consider i being
object such that A2:
(
i in dom p &
z = p . i )
by FUNCT_1:def 3;
reconsider i =
i as
Nat by A2;
reconsider ppi =
p . i as
DecoratedTree by A2, TREES_3:24;
A3:
( 1
<= i &
i <= len p )
by A2, FINSEQ_3:25;
then A4:
(i -' 1) + 1
= i
by XREAL_1:235;
then A5:
i -' 1
< len p
by A3, NAT_1:13;
A6:
len (doms p) = len p
by TREES_3:38;
A7:
(doms p) . i = dom ppi
by A2, FUNCT_6:22;
A8:
dom e = tree (doms p)
by TREES_4:10;
(
<*(i -' 1)*> ^ (<*> NAT) = <*(i -' 1)*> &
<*> NAT in dom ppi )
by FINSEQ_1:34, TREES_1:22;
then reconsider q =
<*(i -' 1)*> as
Element of
dom e by A4, A5, A6, A7, A8, TREES_3:def 15;
e | q = z
by A2, A4, A5, TREES_4:def 4;
then
z is
Element of
(Free (S,Y))
by MSAFREE3:33;
hence
z in X
by A1;
verum
end;
hence
p is FinSequence of X
by FINSEQ_1:def 4; verum