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 reconsider f1 = f as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;
assume A2: f = g ; :: thesis: 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; :: thesis: verum