let R be Relation; :: thesis: for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P )
let P be RedSequence of R; :: thesis: ( len P > 1 implies ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) )
assume A1: len P > 1 ; :: thesis: ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P )
consider Q being FinSequence, x being set such that
A2: P = Q ^ <*x*> and
A3: (len Q) + 1 = len P by Th2;
1 + (len Q) > 1 + 0 by A1, A3;
then ( len <*x*> = 1 & len Q > 0 ) by FINSEQ_1:39;
then A4: Q is RedSequence of R by A2, Th4;
P . (len P) = x by A2, A3, FINSEQ_1:42;
hence ex Q being RedSequence of R st
( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) by A2, A3, A4; :: thesis: verum