let I be non empty set ; :: thesis: for R being Relation of I
for r being RedSequence of R st len r > 1 holds
r . (len r) in I
let R be Relation of I; :: thesis: for r being RedSequence of R st len r > 1 holds
r . (len r) in I
let r be RedSequence of R; :: thesis: ( len r > 1 implies r . (len r) in I )
assume Z0: len r > 1 ; :: thesis: r . (len r) in I
then consider i being Nat such that
A1: len r = 1 + i by NAT_1:10;
( len r >= i & i >= 1 ) by Z0, A1, NAT_1:13;
then ( i in dom r & i + 1 in dom r ) by A1, FINSEQ_3:25, FINSEQ_5:6;
then [(r . i),(r . (len r))] in R by A1, REWRITE1:def 2;
hence r . (len r) in I by ZFMISC_1:87; :: thesis: verum