theorem Th7: :: MATRTOP3:7

for i, n being Nat st i in Seg n holds
( AxialSymmetry (i,n) is diagonal & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) )