let R be Relation; :: thesis: for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P )
let P be RedSequence of R; :: thesis: ( len P > 1 implies ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) )
assume A1: len P > 1 ; :: thesis: ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P )
consider x being object , Q being FinSequence such that
A2: P = <*x*> ^ Q and
A3: len P = (len Q) + 1 by REWRITE1:5;
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 . 1 = x by A2, FINSEQ_1:41;
hence ex Q being RedSequence of R st
( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) by A2, A3, A4; :: thesis: verum