now :: thesis: for i being set st i in I holds
(id A) . i is one-to-one

let i be set ; :: thesis: ( i in I implies (id A) . i is one-to-one )
assume i in I ; :: thesis: (id A) . i is one-to-one
then (id A) . i = id (A . i) by MSUALG_3:def 1;
hence (id A) . i is one-to-one ; :: thesis: verum

end;

hence id A is "1-1" by MSUALG_3:1; :: thesis: verum