let r be Real; :: thesis: for i, j, k, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k <> i & k <> j holds
((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k
let i, j, k, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k <> i & k <> j holds
((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k
let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n & k <> i & k <> j implies ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k )
set O = Rotation (i,j,n,r);
set M = Mx2Tran (Rotation (i,j,n,r));
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
set S = Seg n;
assume A1: ( 1 <= i & i < j & j <= n & k <> i & k <> j ) ; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k
len ((Mx2Tran (Rotation (i,j,n,r))) . p) = n by CARD_1:def 7;
then A2: dom ((Mx2Tran (Rotation (i,j,n,r))) . 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 ( k in Seg n or not k in Seg n ) ;

suppose A4: k in Seg n ; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k

then ( 1 <= k & k <= n ) by FINSEQ_1:1;
hence ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) by MATRTOP1:18
.= p . k by A1, A4, Th14 ;
:: thesis: verum

end;

suppose A5: not k in Seg n ; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k

then ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = {} by A2, FUNCT_1:def 2;
hence ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k by A3, A5, FUNCT_1:def 2; :: thesis: verum

end;

end;