let X be non empty set ; :: thesis: for R being Relation of X
for x being Element of X
for y being set st R reduces x,y holds
y in X
let R be Relation of X; :: thesis: for x being Element of X
for y being set st R reduces x,y holds
y in X
let x be Element of X; :: thesis: for y being set st R reduces x,y holds
y in X
let y be set ; :: thesis: ( R reduces x,y implies y in X )
given p being RedSequence of R such that A1: p . 1 = x and
A2: p . (len p) = y ; :: according to REWRITE1:def 3 :: thesis: y in X
len p >= 0 + 1 by NAT_1:13;
then len p in dom p by FINSEQ_3:25;
then A3: y in rng p by A2, FUNCT_1:3;
p is FinSequence of X by A1, Th73;
then rng p c= X by FINSEQ_1:def 4;
hence y in X by A3; :: thesis: verum