set A = the ManySortedSet of I;

take F = id the ManySortedSet of I; :: thesis: F is "1-1"

let i be set ; :: according to MSUALG_3:def 2 :: thesis: for f being Function st i in dom F & F . i = f holds

f is one-to-one

let f be Function; :: thesis: ( i in dom F & F . i = f implies f is one-to-one )

A1: dom (id the ManySortedSet of I) = I by PARTFUN1:def 2;

assume ( i in dom F & F . i = f ) ; :: thesis: f is one-to-one

then f = id ( the ManySortedSet of I . i) by A1, Def1;

hence f is one-to-one ; :: thesis: verum

take F = id the ManySortedSet of I; :: thesis: F is "1-1"

let i be set ; :: according to MSUALG_3:def 2 :: thesis: for f being Function st i in dom F & F . i = f holds

f is one-to-one

let f be Function; :: thesis: ( i in dom F & F . i = f implies f is one-to-one )

A1: dom (id the ManySortedSet of I) = I by PARTFUN1:def 2;

assume ( i in dom F & F . i = f ) ; :: thesis: f is one-to-one

then f = id ( the ManySortedSet of I . i) by A1, Def1;

hence f is one-to-one ; :: thesis: verum