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 A4: f = g ; :: thesis: f " = g "
then f1 = g ;
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 FUNCT_2:def 3;
A7: g1 * f = (g ") * f1 by A1, A5, Def9
.= id (dom f1) by A4, A6, TOPS_2:65
.= id (RLMSpace n) by FUNCT_2:def 1
.= 1_ (IsomGroup n) by Th10 ;
f * g1 = f1 * (g ") by A1, A5, Def9
.= id (RLMSpace n) by A4, A6, TOPS_2:65
.= 1_ (IsomGroup n) by Th10 ;
hence f " = g " by A7, GROUP_1:12; :: thesis: verum