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)

(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

hence
(Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2))
by MATRIX_0:27; :: thesis: verum
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;

end;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 ) )
;

end;

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;

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

end;

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;.= ((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

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;.= ((- (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

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;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

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;

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

end;

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;.= ((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

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;.= ((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

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;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

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;

end;A34: [k,m] in [:(Seg n),(Seg n):] by A11, MATRIX_0:24;

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

end;

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;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

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;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