let R be Relation; :: thesis: for a being object holds R reduces a,a
let a be object ; :: thesis: R reduces a,a
reconsider p = <*a*> as RedSequence of R by Th6;
take p ; :: according to REWRITE1:def 3 :: thesis: ( p . 1 = a & p . (len p) = a )
len p = 1 by FINSEQ_1:40;
hence ( p . 1 = a & p . (len p) = a ) by FINSEQ_1:40; :: thesis: verum