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