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

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