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

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