let r1, r2 be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))
let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2)) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= n ; :: thesis: (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))
set S = Seg n;
1 <= j by A1, A2, XXREAL_0:2;
then A4: j in Seg n by A3;
set O1 = Rotation (i,j,n,r1);
set O2 = Rotation (i,j,n,r2);
set O = Rotation (i,j,n,(r1 + r2));
set O12 = (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2));
A5: width (Rotation (i,j,n,r1)) = n by MATRIX_0:24;
i <= n by A2, A3, XXREAL_0:2;
then A6: i in Seg n by A1;
A7: Indices (Rotation (i,j,n,r1)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A8: Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A9: Indices (Rotation (i,j,n,(r1 + r2))) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A10: len (Rotation (i,j,n,r2)) = n by MATRIX_0:25;
for k, m being Nat st [k,m] in Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) holds
((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

proof

let k, m be Nat; :: thesis: ( [k,m] in Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) implies ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m) )
assume A11: [k,m] in Indices ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)
then A12: k in Seg n by A8, ZFMISC_1:87;
A13: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Line ((Rotation (i,j,n,r1)),k)) "*" (Col ((Rotation (i,j,n,r2)),m)) by A5, A10, A11, MATRIX_3:def 4;
len (@ (Line ((Rotation (i,j,n,r1)),k))) = n by A5, CARD_1:def 7;
then reconsider L = @ (Line ((Rotation (i,j,n,r1)),k)) as Element of (TOP-REAL n) by TOPREAL3:46;
A14: m in Seg n by A8, A11, ZFMISC_1:87;
then A15: L . m = (Rotation (i,j,n,r1)) * (k,m) by A5, MATRIX_0:def 7;
A16: @ L = Line ((Rotation (i,j,n,r1)),k) ;
A17: L . i = (Rotation (i,j,n,r1)) * (k,i) by A5, A6, MATRIX_0:def 7;
A18: L . j = (Rotation (i,j,n,r1)) * (k,j) by A4, A5, MATRIX_0:def 7;

per cases ( m = i or m = j or ( m <> i & m <> j ) ) ;

suppose A19: m = i ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

then A20: (Line ((Rotation (i,j,n,r1)),k)) "*" (Col ((Rotation (i,j,n,r2)),m)) = ((L . i) * (cos r2)) + ((L . j) * (- (sin r2))) by A1, A2, A3, A16, Th15;

per cases ( k = i or k = j or ( k <> j & k <> i ) ) ;

suppose A21: k = i ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = ((cos r1) * (cos r2)) + ((L . j) * (- (sin r2))) by A1, A2, A3, A13, A17, A20, Def3
.= ((cos r1) * (cos r2)) + ((sin r1) * (- (sin r2))) by A1, A2, A3, A18, A21, Def3
.= ((cos r1) * (cos r2)) - ((sin r1) * (sin r2))
.= cos (r1 + r2) by SIN_COS:75
.= (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A19, A21, Def3 ;
:: thesis: verum

end;

suppose A22: k = j ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = ((- (sin r1)) * (cos r2)) + ((L . j) * (- (sin r2))) by A1, A2, A3, A13, A17, A20, Def3
.= ((- (sin r1)) * (cos r2)) + ((cos r1) * (- (sin r2))) by A1, A2, A3, A18, A22, Def3
.= - (((sin r1) * (cos r2)) + ((cos r1) * (sin r2)))
.= - (sin (r1 + r2)) by SIN_COS:75
.= (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A19, A22, Def3 ;
:: thesis: verum

end;

suppose ( k <> j & k <> i ) ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

then not k in {i,j} by TARSKI:def 2;
then A23: ( {k,i} <> {i,j} & {k,j} <> {i,j} ) by TARSKI:def 2;
A24: [k,j] in [:(Seg n),(Seg n):] by A4, A12, ZFMISC_1:87;
A25: [k,i] in [:(Seg n),(Seg n):] by A6, A12, ZFMISC_1:87;
then (Rotation (i,j,n,r1)) * (k,i) = 0. F_Real by A1, A2, A3, A7, A23, Def3;
hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (0 * (cos r2)) + (0 * (- (sin r2))) by A1, A2, A3, A7, A13, A17, A18, A20, A23, A24, Def3
.= (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A9, A19, A23, A25, Def3 ;
:: thesis: verum

end;

end;

end;

suppose A26: m = j ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

then A27: (Line ((Rotation (i,j,n,r1)),k)) "*" (Col ((Rotation (i,j,n,r2)),m)) = ((L . i) * (sin r2)) + ((L . j) * (cos r2)) by A1, A2, A3, A16, Th16;

per cases ( k = i or k = j or ( k <> j & k <> i ) ) ;

suppose A28: k = i ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = ((cos r1) * (sin r2)) + ((L . j) * (cos r2)) by A1, A2, A3, A13, A17, A27, Def3
.= ((cos r1) * (sin r2)) + ((sin r1) * (cos r2)) by A1, A2, A3, A18, A28, Def3
.= sin (r1 + r2) by SIN_COS:75
.= (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A26, A28, Def3 ;
:: thesis: verum

end;

suppose A29: k = j ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = ((- (sin r1)) * (sin r2)) + ((L . j) * (cos r2)) by A1, A2, A3, A13, A17, A27, Def3
.= ((cos r1) * (cos r2)) - ((sin r1) * (sin r2)) by A1, A2, A3, A18, A29, Def3
.= cos (r1 + r2) by SIN_COS:75
.= (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A26, A29, Def3 ;
:: thesis: verum

end;

suppose ( k <> j & k <> i ) ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

then not k in {i,j} by TARSKI:def 2;
then A30: ( {k,i} <> {i,j} & {k,j} <> {i,j} ) by TARSKI:def 2;
A31: [k,j] in [:(Seg n),(Seg n):] by A4, A12, ZFMISC_1:87;
[k,i] in [:(Seg n),(Seg n):] by A6, A12, ZFMISC_1:87;
then (Rotation (i,j,n,r1)) * (k,i) = 0. F_Real by A1, A2, A3, A7, A30, Def3;
hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (0 * (sin r2)) + (0 * (cos r2)) by A1, A2, A3, A7, A13, A17, A18, A27, A30, A31, Def3
.= (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A9, A26, A30, A31, Def3 ;
:: thesis: verum

end;

end;

end;

suppose A32: ( m <> i & m <> j ) ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

then A33: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = L . m by A1, A2, A3, A13, A14, A16, Th14;
A34: [k,m] in [:(Seg n),(Seg n):] by A11, MATRIX_0:24;

per cases ( k = m or k <> m ) ;

suppose A35: k = m ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

then (Rotation (i,j,n,r1)) * (k,m) = 1. F_Real by A1, A2, A3, A7, A8, A11, A32, Def3;
hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A9, A15, A32, A33, A34, A35, Def3; :: thesis: verum

end;

suppose A36: k <> m ; :: thesis: ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m)

not m in {i,j} by A32, TARSKI:def 2;
then A37: {k,m} <> {i,j} by TARSKI:def 2;
then (Rotation (i,j,n,r1)) * (k,m) = 0. F_Real by A1, A2, A3, A7, A8, A11, A36, Def3;
hence ((Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2))) * (k,m) = (Rotation (i,j,n,(r1 + r2))) * (k,m) by A1, A2, A3, A9, A15, A33, A34, A36, A37, Def3; :: thesis: verum

end;

end;

end;

end;

end;

hence (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2)) by MATRIX_0:27; :: thesis: verum