let S be non empty non void ManySortedSign ; :: thesis: for Y being empty-yielding 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 empty-yielding ManySortedSet of the carrier of S; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: ( not o -tree p in X or p is FinSequence of X )
assume o -tree p in X ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in X )
assume z in rng p ; :: thesis: 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; :: thesis: verum

end;

hence p is FinSequence of X by FINSEQ_1:def 4; :: thesis: verum