set S = SubIsomGroupRel G;

set X = the carrier of (RLMSpace n);

then A3: field (SubIsomGroupRel G) = the carrier of (RLMSpace n) by ORDERS_1:13;

dom (SubIsomGroupRel G) = the carrier of (RLMSpace n) by A2, ORDERS_1:13;

hence SubIsomGroupRel G is total by PARTFUN1:def 2; :: thesis: ( SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive )

hence SubIsomGroupRel G is symmetric by A3, RELAT_2:def 11; :: thesis: SubIsomGroupRel G is transitive

hence SubIsomGroupRel G is transitive by A3, RELAT_2:def 16; :: thesis: verum

set X = the carrier of (RLMSpace n);

now :: thesis: for x being object st x in the carrier of (RLMSpace n) holds

[x,x] in SubIsomGroupRel G

then A2:
SubIsomGroupRel G is_reflexive_in the carrier of (RLMSpace n)
by RELAT_2:def 1;[x,x] in SubIsomGroupRel G

let x be object ; :: thesis: ( x in the carrier of (RLMSpace n) implies [x,x] in SubIsomGroupRel G )

assume x in the carrier of (RLMSpace n) ; :: thesis: [x,x] in SubIsomGroupRel G

then reconsider x1 = x as Element of (RLMSpace n) ;

1_ (IsomGroup n) = id (RLMSpace n) by Th7;

then id (RLMSpace n) in G by GROUP_2:46;

then A1: id (RLMSpace n) in the carrier of G ;

(id (RLMSpace n)) . x1 = x1 ;

hence [x,x] in SubIsomGroupRel G by A1, Def10; :: thesis: verum

end;assume x in the carrier of (RLMSpace n) ; :: thesis: [x,x] in SubIsomGroupRel G

then reconsider x1 = x as Element of (RLMSpace n) ;

1_ (IsomGroup n) = id (RLMSpace n) by Th7;

then id (RLMSpace n) in G by GROUP_2:46;

then A1: id (RLMSpace n) in the carrier of G ;

(id (RLMSpace n)) . x1 = x1 ;

hence [x,x] in SubIsomGroupRel G by A1, Def10; :: thesis: verum

then A3: field (SubIsomGroupRel G) = the carrier of (RLMSpace n) by ORDERS_1:13;

dom (SubIsomGroupRel G) = the carrier of (RLMSpace n) by A2, ORDERS_1:13;

hence SubIsomGroupRel G is total by PARTFUN1:def 2; :: thesis: ( SubIsomGroupRel G is symmetric & SubIsomGroupRel G is transitive )

now :: thesis: for x, y being object st x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G holds

[y,x] in SubIsomGroupRel G

then
SubIsomGroupRel G is_symmetric_in the carrier of (RLMSpace n)
by RELAT_2:def 3;[y,x] in SubIsomGroupRel G

let x, y be object ; :: thesis: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G implies [y,x] in SubIsomGroupRel G )

assume that

A4: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) ) and

A5: [x,y] in SubIsomGroupRel G ; :: thesis: [y,x] in SubIsomGroupRel G

reconsider x1 = x, y1 = y as Element of (RLMSpace n) by A4;

consider f being Function such that

A6: f in the carrier of G and

A7: f . x1 = y1 by A5, Def10;

reconsider f1 = f as Element of G by A6;

A8: the carrier of G c= the carrier of (IsomGroup n) by GROUP_2:def 5;

then reconsider f3 = f1 as Element of (IsomGroup n) ;

f in the carrier of (IsomGroup n) by A6, A8;

then f in ISOM (RLMSpace n) by Def9;

then reconsider f2 = f as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

x1 in the carrier of (RLMSpace n) ;

then x1 in dom f2 by FUNCT_2:def 1;

then A9: (f ") . y1 = x1 by A7, FUNCT_1:34;

f1 " = f3 " by GROUP_2:48

.= f2 " by Th8

.= f " by TOPS_2:def 4 ;

hence [y,x] in SubIsomGroupRel G by A9, Def10; :: thesis: verum

end;assume that

A4: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) ) and

A5: [x,y] in SubIsomGroupRel G ; :: thesis: [y,x] in SubIsomGroupRel G

reconsider x1 = x, y1 = y as Element of (RLMSpace n) by A4;

consider f being Function such that

A6: f in the carrier of G and

A7: f . x1 = y1 by A5, Def10;

reconsider f1 = f as Element of G by A6;

A8: the carrier of G c= the carrier of (IsomGroup n) by GROUP_2:def 5;

then reconsider f3 = f1 as Element of (IsomGroup n) ;

f in the carrier of (IsomGroup n) by A6, A8;

then f in ISOM (RLMSpace n) by Def9;

then reconsider f2 = f as onto isometric Function of (RLMSpace n),(RLMSpace n) by Def4;

x1 in the carrier of (RLMSpace n) ;

then x1 in dom f2 by FUNCT_2:def 1;

then A9: (f ") . y1 = x1 by A7, FUNCT_1:34;

f1 " = f3 " by GROUP_2:48

.= f2 " by Th8

.= f " by TOPS_2:def 4 ;

hence [y,x] in SubIsomGroupRel G by A9, Def10; :: thesis: verum

hence SubIsomGroupRel G is symmetric by A3, RELAT_2:def 11; :: thesis: SubIsomGroupRel G is transitive

now :: thesis: for x, y, z being object st x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G & [y,z] in SubIsomGroupRel G holds

[x,z] in SubIsomGroupRel G

then
SubIsomGroupRel G is_transitive_in the carrier of (RLMSpace n)
by RELAT_2:def 8;[x,z] in SubIsomGroupRel G

let x, y, z be object ; :: thesis: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) & [x,y] in SubIsomGroupRel G & [y,z] in SubIsomGroupRel G implies [x,z] in SubIsomGroupRel G )

assume that

A10: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) ) and

A11: [x,y] in SubIsomGroupRel G and

A12: [y,z] in SubIsomGroupRel G ; :: thesis: [x,z] in SubIsomGroupRel G

reconsider x1 = x, y1 = y, z1 = z as Element of (RLMSpace n) by A10;

consider f being Function such that

A13: f in the carrier of G and

A14: f . x1 = y1 by A11, Def10;

reconsider f2 = f as Element of G by A13;

A15: the carrier of G c= the carrier of (IsomGroup n) by GROUP_2:def 5;

then reconsider f3 = f2 as Element of (IsomGroup n) ;

f in the carrier of (IsomGroup n) by A13, A15;

then A16: f in ISOM (RLMSpace n) by Def9;

consider g being Function such that

A17: g in the carrier of G and

A18: g . y1 = z1 by A12, Def10;

reconsider g2 = g as Element of G by A17;

A19: x1 in the carrier of (RLMSpace n) ;

reconsider g3 = g2 as Element of (IsomGroup n) by A15;

( f2 in G & g2 in G ) ;

then A20: g3 * f3 in G by GROUP_2:50;

g in the carrier of (IsomGroup n) by A17, A15;

then g in ISOM (RLMSpace n) by Def9;

then g3 * f3 = g * f by A16, Def9;

then A21: g * f in the carrier of G by A20;

f is onto isometric Function of (RLMSpace n),(RLMSpace n) by A16, Def4;

then x1 in dom f by A19, FUNCT_2:def 1;

then (g * f) . x1 = z1 by A14, A18, FUNCT_1:13;

hence [x,z] in SubIsomGroupRel G by A21, Def10; :: thesis: verum

end;assume that

A10: ( x in the carrier of (RLMSpace n) & y in the carrier of (RLMSpace n) & z in the carrier of (RLMSpace n) ) and

A11: [x,y] in SubIsomGroupRel G and

A12: [y,z] in SubIsomGroupRel G ; :: thesis: [x,z] in SubIsomGroupRel G

reconsider x1 = x, y1 = y, z1 = z as Element of (RLMSpace n) by A10;

consider f being Function such that

A13: f in the carrier of G and

A14: f . x1 = y1 by A11, Def10;

reconsider f2 = f as Element of G by A13;

A15: the carrier of G c= the carrier of (IsomGroup n) by GROUP_2:def 5;

then reconsider f3 = f2 as Element of (IsomGroup n) ;

f in the carrier of (IsomGroup n) by A13, A15;

then A16: f in ISOM (RLMSpace n) by Def9;

consider g being Function such that

A17: g in the carrier of G and

A18: g . y1 = z1 by A12, Def10;

reconsider g2 = g as Element of G by A17;

A19: x1 in the carrier of (RLMSpace n) ;

reconsider g3 = g2 as Element of (IsomGroup n) by A15;

( f2 in G & g2 in G ) ;

then A20: g3 * f3 in G by GROUP_2:50;

g in the carrier of (IsomGroup n) by A17, A15;

then g in ISOM (RLMSpace n) by Def9;

then g3 * f3 = g * f by A16, Def9;

then A21: g * f in the carrier of G by A20;

f is onto isometric Function of (RLMSpace n),(RLMSpace n) by A16, Def4;

then x1 in dom f by A19, FUNCT_2:def 1;

then (g * f) . x1 = z1 by A14, A18, FUNCT_1:13;

hence [x,z] in SubIsomGroupRel G by A21, Def10; :: thesis: verum

hence SubIsomGroupRel G is transitive by A3, RELAT_2:def 16; :: thesis: verum