( rng (X |` R) c= rng R & rng R c= A ) by Def17, Th80, XTUPLE_0:9;
hence rng (X |` R) c= A ; :: according to RELAT_1:def 19 :: thesis: X |` R is X -valued
thus rng (X |` R) c= X by Th78; :: according to RELAT_1:def 19 :: thesis: verum