let x be set ; :: thesis: for U, U1 being non empty set st (U -multiCat) . x is U1 -valued & x in (U *) * holds
x is FinSequence of U1 *
let U, U1 be non empty set ; :: thesis: ( (U -multiCat) . x is U1 -valued & x in (U *) * implies x is FinSequence of U1 * )
set C = U -multiCat ;
set f = U -concatenation ;
set F = MultPlace (U -concatenation);
set D = U * ;
{} null (U *) is U * -valued Relation ;
then reconsider e = {} as U * -valued FinSequence ;
defpred S₁[ Nat] means for p being U * -valued $1 + 1 -element FinSequence st (U -multiCat) . p is U1 -valued holds
p is U1 * -valued ;
A1: S₁[ 0 ]

proof

let p be U * -valued 0 + 1 -element FinSequence; :: thesis: ( (U -multiCat) . p is U1 -valued implies p is U1 * -valued )
reconsider ppp = p as U * -valued 1 + 0 -element FinSequence ;
{(ppp . 1)} \ (U *) = {} ;
then reconsider p1 = p . 1 as Element of U * by ZFMISC_1:60;
A2: len p = 1 by CARD_1:def 7;
p = {} ^ <*(p . 1)*> by A2, FINSEQ_1:40;
then A3: (U -multiCat) . p = ((U -multiCat) . e) ^ p1 by Th33
.= {} ^ (p . 1)
.= p . 1 ;
p is 1 -element FinSequence of U * by Lm1;
then reconsider pp = p as 1 -element Element of (U *) * ;
assume (U -multiCat) . p is U1 -valued ; :: thesis: p is U1 * -valued
then reconsider u1 = (U -multiCat) . pp as FinSequence of U1 by Lm1;
u1 = p . 1 by A3;
then reconsider q = p . 1 as Element of U1 * ;
<*q*> is FinSequence of U1 * ;
hence p is U1 * -valued by A2, FINSEQ_1:40; :: thesis: verum

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider NN = n + 1 as non zero Element of NAT by ORDINAL1:def 12;
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
let p be U * -valued (n + 1) + 1 -element FinSequence; :: thesis: ( (U -multiCat) . p is U1 -valued implies p is U1 * -valued )
assume A6: (U -multiCat) . p is U1 -valued ; :: thesis: p is U1 * -valued
reconsider pp = p null p as U * -valued n + 2 -element FinSequence ;
reconsider ppp = pp as U * -valued NN + 1 -element FinSequence ;
reconsider pppp = ppp as U * -valued (NN + 1) + 0 -element FinSequence ;
reconsider p1 = ppp | (Seg NN) as U * -valued NN -element FinSequence ;
{(pppp . (NN + 1))} \ (U *) = {} ;
then reconsider u = ppp . (NN + 1) as Element of U * by ZFMISC_1:60;
A7: ppp \+\ (p1 ^ <*(ppp . (NN + 1))*>) = {} ;
then p = p1 ^ <*u*> by Th29;
then A8: (U -multiCat) . p = ((U -multiCat) . p1) ^ u by Th33;
then ( rng ((U -multiCat) . p) c= U1 & rng ((U -multiCat) . p1) c= rng ((U -multiCat) . p) ) by A6, FINSEQ_1:29;
then reconsider q = (U -multiCat) . p1 as U1 -valued FinSequence by XBOOLE_1:1, RELAT_1:def 19;
q is U1 -valued ;
then reconsider p11 = p1 as U1 * -valued NN -element FinSequence by A5;
( rng u c= rng ((U -multiCat) . p) & rng ((U -multiCat) . p) c= U1 ) by A8, FINSEQ_1:30, A6;
then u is U1 -valued by XBOOLE_1:1;
then u is FinSequence of U1 by Lm1;
then reconsider uu = u as Element of U1 * ;
p11 ^ <*uu*> is U1 * -valued ;
hence p is U1 * -valued by A7, Th29; :: thesis: verum

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
assume A10: ( (U -multiCat) . x is U1 -valued & x in (U *) * ) ; :: thesis: x is FinSequence of U1 *

per cases ( x is empty or not x is empty ) ;

suppose x is empty ; :: thesis: x is FinSequence of U1 *

then reconsider xx = x as empty set ;
xx null (U1 *) is U1 * -valued FinSequence ;
hence x is FinSequence of U1 * by Lm1; :: thesis: verum

end;

suppose not x is empty ; :: thesis: x is FinSequence of U1 *

then reconsider xx = x as U * -valued non empty FinSequence by A10;
consider m being Nat such that
A11: len xx = m + 1 by NAT_1:6;
xx null {} is m + 1 -element by A11;
then reconsider xxx = xx as U * -valued m + 1 -element FinSequence ;
xxx is U1 * -valued by A10, A9;
hence x is FinSequence of U1 * by Lm1; :: thesis: verum

end;

end;