let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in I or rng ((id A) . i) = A . i )
assume i in I ; :: thesis: rng ((id A) . i) = A . i
then (id A) . i = id (A . i) by MSUALG_3:def 1;
hence rng ((id A) . i) = A . i by RELAT_1:45; :: thesis: verum