let i, j, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n & i <> j holds
((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n & i <> j implies ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j )
set A = AxialSymmetry (i,n);
set M = Mx2Tran (AxialSymmetry (i,n));
set Mp = (Mx2Tran (AxialSymmetry (i,n))) . p;
set S = Seg n;
assume A1: ( i in Seg n & i <> j ) ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j
len ((Mx2Tran (AxialSymmetry (i,n))) . p) = n by CARD_1:def 7;
then A2: dom ((Mx2Tran (AxialSymmetry (i,n))) . p) = Seg n by FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then A3: dom p = Seg n by FINSEQ_1:def 3;
per cases ( j in Seg n or not j in Seg n ) ;
suppose A4: j in Seg n ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j
then ( 1 <= j & j <= n ) by FINSEQ_1:1;
hence ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) by MATRTOP1:18
.= p . j by A1, A4, Th5 ;
:: thesis: verum
end;
suppose A5: not j in Seg n ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j
then ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = {} by A2, FUNCT_1:def 2;
hence ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j by A3, A5, FUNCT_1:def 2; :: thesis: verum
end;
end;