let n be Element of NAT ; for f being Element of (IsomGroup n)
for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds
f " = g "
let f be Element of (IsomGroup n); for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds
f " = g "
let g be Function of (RLMSpace n),(RLMSpace n); ( f = g implies f " = g " )
f in the carrier of (IsomGroup n)
;
then A1:
f in ISOM (RLMSpace n)
by Def9;
then reconsider f1 = f as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;
assume A2:
f = g
; f " = g "
then
f1 = g
;
then A3:
g " in ISOM (RLMSpace n)
by Def4;
then reconsider g1 = g " as Element of (IsomGroup n) by Def9;
A4:
rng f1 = [#] (RLMSpace n)
by FUNCT_2:def 3;
A5: g1 * f =
(g ") * f1
by A1, A3, Def9
.=
id (dom f1)
by A2, A4, TOPS_2:52
.=
id (RLMSpace n)
by FUNCT_2:def 1
.=
1_ (IsomGroup n)
by Th7
;
f * g1 =
f1 * (g ")
by A1, A3, Def9
.=
id (RLMSpace n)
by A2, A4, TOPS_2:52
.=
1_ (IsomGroup n)
by Th7
;
hence
f " = g "
by A5, GROUP_1:5; verum