let R be Relation; :: thesis: for P being RedSequence of R st len P > 1 holds
ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
let P be RedSequence of R; :: thesis: ( len P > 1 implies ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) ) )
assume len P > 1 ; :: thesis: ex Q being RedSequence of R st
( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
then consider Q being RedSequence of R such that
A1: ( P = <*(P . 1)*> ^ Q & (len Q) + 1 = len P ) by Th5;
take Q ; :: thesis: ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) )
thus ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds
Q . k = P . (k + 1) ) ) by A1, Th1; :: thesis: verum