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