let I be set ; :: thesis: for F being ManySortedFunction of I holds

( F is "1-1" iff for i being set st i in I holds

F . i is one-to-one )

let F be ManySortedFunction of I; :: thesis: ( F is "1-1" iff for i being set st i in I holds

F . i is one-to-one )

A1: dom F = I by PARTFUN1:def 2;

hence ( F is "1-1" implies for i being set st i in I holds

F . i is one-to-one ) ; :: thesis: ( ( for i being set st i in I holds

F . i is one-to-one ) implies F is "1-1" )

assume for i being set st i in I holds

F . i is one-to-one ; :: thesis: F is "1-1"

then for i being set

for f being Function st i in dom F & f = F . i holds

f is one-to-one by A1;

hence F is "1-1" ; :: thesis: verum

( F is "1-1" iff for i being set st i in I holds

F . i is one-to-one )

let F be ManySortedFunction of I; :: thesis: ( F is "1-1" iff for i being set st i in I holds

F . i is one-to-one )

A1: dom F = I by PARTFUN1:def 2;

hence ( F is "1-1" implies for i being set st i in I holds

F . i is one-to-one ) ; :: thesis: ( ( for i being set st i in I holds

F . i is one-to-one ) implies F is "1-1" )

assume for i being set st i in I holds

F . i is one-to-one ; :: thesis: F is "1-1"

then for i being set

for f being Function st i in dom F & f = F . i holds

f is one-to-one by A1;

hence F is "1-1" ; :: thesis: verum