let X, o be set ; for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free C,(MSVars C)) & 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 C,(MSVars C)) & 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 C,(MSVars C))
; ( 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 expression of C by A1;
rng p c= X
proof
let z be
set ;
TARSKI:def 3 ( not z in rng p or z in X )
assume
z in rng p
;
z in X
then consider i being
set such that A2:
(
i in dom p &
z = p . i )
by FUNCT_1:def 5;
reconsider i =
i as
Nat by A2;
reconsider ppi =
p . i as
DecoratedTree by A2, TREES_3:26;
B1:
( 1
<= i &
i <= len p )
by A2, FINSEQ_3:27;
then A3:
(i -' 1) + 1
= i
by XREAL_1:237;
then B2:
i -' 1
< len p
by B1, NAT_1:13;
A4:
len (doms p) = len p
by TREES_3:40;
A5:
(doms p) . i = dom ppi
by A2, FUNCT_6:31;
A6:
dom e = tree (doms p)
by TREES_4:10;
(
<*(i -' 1)*> ^ (<*> NAT ) = <*(i -' 1)*> &
<*> NAT in dom ppi )
by FINSEQ_1:47, TREES_1:47;
then reconsider q =
<*(i -' 1)*> as
Element of
dom e by A3, B2, A4, A5, A6, TREES_3:def 15;
e | q = z
by A2, A3, B2, TREES_4:def 4;
then
z is
Element of
(Free C,(MSVars C))
by MSAFREE3:34;
hence
z in X
by A1;
verum
end;
hence
p is FinSequence of X
by FINSEQ_1:def 4; verum