now :: thesis: for i being set st i in I holds

(id A) . i is one-to-one

hence
id A is "1-1"
by MSUALG_3:1; :: thesis: verum(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;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