let
f
,
g
be
one-to-one
Function
;
:: thesis:
(
f
"
=
g
"
implies
f
=
g
)
(
(
f
"
)
"
=
f
&
(
g
"
)
"
=
g
)
by
FUNCT_1:43
;
hence
(
f
"
=
g
"
implies
f
=
g
) ;
:: thesis:
verum