let n be Element of NAT ; :: thesis: 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); :: thesis: for g being Function of (RLMSpace n),(RLMSpace n) st f = g holds
f " = g "
let g be Function of (RLMSpace n),(RLMSpace n); :: thesis: ( f = g implies f " = g " )
f in the carrier of (IsomGroup n) ;
then A1: f in ISOM (RLMSpace n) by Def9;
then consider f1 being Function of (RLMSpace n),(RLMSpace n) such that
A2: f1 = f and
A3: f1 is isometric by Def4;
assume A4: f = g ; :: thesis: f " = g "
then g " is isometric by A2, A3, Th3;
then A5: g " in ISOM (RLMSpace n) by Def4;
then reconsider g1 = g " as Element of (IsomGroup n) by Def9;
A6: rng f1 = [#] (RLMSpace n) by A3, Def3;
A7: g1 * f = (g " ) * f1 by A1, A2, A5, Def9
.= id (dom f1) by A4, A2, A3, A6, TOPS_2:65
.= id (RLMSpace n) by FUNCT_2:def 1
.= 1_ (IsomGroup n) by Th10 ;
f * g1 = f1 * (g " ) by A1, A2, A5, Def9
.= id (RLMSpace n) by A4, A2, A3, A6, TOPS_2:65
.= 1_ (IsomGroup n) by Th10 ;
hence f " = g " by A7, GROUP_1:12; :: thesis: verum