let A be non empty set ; :: thesis: for R being Relation of A
for t being RedSequence of R holds
( t . 1 in A iff t is A -valued )
let R be Relation of A; :: thesis: for t being RedSequence of R holds
( t . 1 in A iff t is A -valued )
let t be RedSequence of R; :: thesis: ( t . 1 in A iff t is A -valued )
rng t <> {} ;
then 1 in dom t by FINSEQ_3:32;
then A1: t . 1 in rng t by FUNCT_1:def 3;

hereby :: thesis: ( t is A -valued implies t . 1 in A )

assume A2: t . 1 in A ; :: thesis: t is A -valued
defpred S₁[ Nat] means ( $1 in dom t implies t . $1 in A );
A3: S₁[ 0 ] by FINSEQ_3:24;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
assume A5: ( i + 1 in dom t & t . (i + 1) nin A ) ; :: thesis: contradiction
( i = 0 or i >= 0 + 1 ) by NAT_1:13;
then consider j being Nat such that
A6: i = j + 1 by A2, A5, NAT_1:6;
( i <= i + 1 & i + 1 <= len t ) by A5, FINSEQ_3:25, NAT_1:11;
then ( 1 <= i & i <= len t ) by A6, NAT_1:11, XXREAL_0:2;
then i in dom t by FINSEQ_3:25;
then [(t . i),(t . (i + 1))] in R by A5, REWRITE1:def 2;
hence contradiction by A5, ZFMISC_1:87; :: thesis: verum

end;

A7: for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
thus t is A -valued :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in rng t or x in A )
assume x in rng t ; :: thesis: x in A
then consider y being object such that
A8: ( y in dom t & x = t . y ) by FUNCT_1:def 3;
reconsider y = y as Nat by A8;
thus x in A by A8, A7; :: thesis: verum

end;

end;

assume rng t c= A ; :: according to RELAT_1:def 19 :: thesis: t . 1 in A
hence t . 1 in A by A1; :: thesis: verum