let X be non empty set ; :: thesis: for R being Relation of X
for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X
let R be Relation of X; :: thesis: for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X
let p be RedSequence of R; :: thesis: ( p . 1 in X implies p is FinSequence of X )
assume A1: p . 1 in X ; :: thesis: p is FinSequence of X
let x be object ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not x in rng p or x in X )
assume x in rng p ; :: thesis: x in X
then consider i being object such that
A2: i in dom p and
A3: x = p . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A2;
A4: i >= 1 by A2, FINSEQ_3:25;

per cases ( i = 1 or i > 1 ) by A4, XXREAL_0:1;

suppose i = 1 ; :: thesis: x in X

hence x in X by A1, A3; :: thesis: verum

end;

suppose i > 1 ; :: thesis: x in X

then i >= 1 + 1 by NAT_1:13;
then consider j being Nat such that
A5: i = (1 + 1) + j by NAT_1:10;
A6: i = (j + 1) + 1 by A5;
A7: j + 1 >= 1 by NAT_1:11;
i <= len p by A2, FINSEQ_3:25;
then j + 1 < len p by A6, NAT_1:13;
then j + 1 in dom p by A7, FINSEQ_3:25;
then [(p . (j + 1)),x] in R by A2, A3, A6, REWRITE1:def 2;
hence x in X by ZFMISC_1:87; :: thesis: verum

end;

end;