let X, Y be set ; :: thesis: ( X c= Y implies for R being X -valued Relation holds R is Y -valued )
assume A1: X c= Y ; :: thesis: for R being X -valued Relation holds R is Y -valued
let R be X -valued Relation; :: thesis: R is Y -valued
rng R c= X by Def17;
hence rng R c= Y by A1; :: according to RELAT_1:def 19 :: thesis: verum