let S, T be RelStr ; :: thesis: for f being Function of S,T st f is one-to-one holds
for R being SubRelStr of S holds f | R is one-to-one
let f be Function of S,T; :: thesis: ( f is one-to-one implies for R being SubRelStr of S holds f | R is one-to-one )
assume A1: f is one-to-one ; :: thesis: for R being SubRelStr of S holds f | R is one-to-one
let R be SubRelStr of S; :: thesis: f | R is one-to-one
f | R = f | the carrier of R by Th6;
hence f | R is one-to-one by A1, FUNCT_1:52; :: thesis: verum