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 ;
B0: 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;
Z0: len p = 1 by CARD_1:def 7;
p = {} ^ <*(p . 1)*> by Z0, FINSEQ_1:40;
then C0: (U -multiCat) . p = ((U -multiCat) . e) ^ p1 by Th33
.= {} ^ (p . 1)
.= p . 1 ;
p is 1 -element FinSequence of U * by Lm45;
then reconsider pp = p as 1 -element Element of (U *) * by FINSEQ_1:def 11;
assume (U -multiCat) . p is U1 -valued ; :: thesis: p is U1 * -valued
then reconsider u1 = (U -multiCat) . pp as FinSequence of U1 by Lm45;
u1 = p . 1 by C0;
then reconsider q = p . 1 as Element of U1 * by FINSEQ_1:def 11;
<*q*> is FinSequence of U1 * ;
hence p is U1 * -valued by Z0, FINSEQ_1:40; :: thesis: verum

end;

B1: 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 C1: 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 C0: (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;
Z0: ppp \+\ (p1 ^ <*(ppp . (NN + 1))*>) = {} ;
then p = p1 ^ <*u*> by Th29;
then C2: (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 C0, FINSEQ_1:29, RELAT_1:def 19;
then rng ((U -multiCat) . p1) c= U1 by XBOOLE_1:1;
then reconsider q = (U -multiCat) . p1 as U1 -valued FinSequence by RELAT_1:def 19;
q is U1 -valued ;
then reconsider p11 = p1 as U1 * -valued NN -element FinSequence by C1;
( rng u c= rng ((U -multiCat) . p) & rng ((U -multiCat) . p) c= U1 ) by C2, C0, FINSEQ_1:30, RELAT_1:def 19;
then rng u c= U1 by XBOOLE_1:1;
then u is U1 -valued by RELAT_1:def 19;
then u is FinSequence of U1 by Lm45;
then reconsider uu = u as Element of U1 * by FINSEQ_1:def 11;
p11 ^ <*uu*> is U1 * -valued ;
hence p is U1 * -valued by Z0, Th29; :: thesis: verum

end;

B3: for n being Nat holds S₁[n] from NAT_1:sch 2(B0, B1);
assume B2: ( (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 Lm45; :: 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 B2;
consider m being Nat such that
C0: len xx = m + 1 by NAT_1:6;
xx null {} is m + 1 -element by C0;
then reconsider xxx = xx as U * -valued m + 1 -element FinSequence ;
xxx is U1 * -valued by B2, B3;
hence x is FinSequence of U1 * by Lm45; :: thesis: verum

end;

end;