let r be Real; :: thesis: for i, j, n being Nat st 1 <= i & i < j & j <= n holds

Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding

let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding )

set M = Mx2Tran (Rotation (i,j,n,r));

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding

let f be Function; :: according to MATRTOP3:def 1 :: thesis: for x being set st f in dom (Mx2Tran (Rotation (i,j,n,r))) & ((Mx2Tran (Rotation (i,j,n,r))) . f) . x <> f . x holds

x in {i,j}

let x be set ; :: thesis: ( f in dom (Mx2Tran (Rotation (i,j,n,r))) & ((Mx2Tran (Rotation (i,j,n,r))) . f) . x <> f . x implies x in {i,j} )

assume that

A2: f in dom (Mx2Tran (Rotation (i,j,n,r))) and

A3: ((Mx2Tran (Rotation (i,j,n,r))) . f) . x <> f . x ; :: thesis: x in {i,j}

reconsider p = f as Point of (TOP-REAL n) by A2, FUNCT_2:52;

len p = n by CARD_1:def 7;

then A4: dom p = Seg n by FINSEQ_1:def 3;

len ((Mx2Tran (Rotation (i,j,n,r))) . p) = n by CARD_1:def 7;

then A5: dom ((Mx2Tran (Rotation (i,j,n,r))) . p) = Seg n by FINSEQ_1:def 3;

Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding

let i, j, n be Nat; :: thesis: ( 1 <= i & i < j & j <= n implies Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding )

set M = Mx2Tran (Rotation (i,j,n,r));

assume A1: ( 1 <= i & i < j & j <= n ) ; :: thesis: Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding

let f be Function; :: according to MATRTOP3:def 1 :: thesis: for x being set st f in dom (Mx2Tran (Rotation (i,j,n,r))) & ((Mx2Tran (Rotation (i,j,n,r))) . f) . x <> f . x holds

x in {i,j}

let x be set ; :: thesis: ( f in dom (Mx2Tran (Rotation (i,j,n,r))) & ((Mx2Tran (Rotation (i,j,n,r))) . f) . x <> f . x implies x in {i,j} )

assume that

A2: f in dom (Mx2Tran (Rotation (i,j,n,r))) and

A3: ((Mx2Tran (Rotation (i,j,n,r))) . f) . x <> f . x ; :: thesis: x in {i,j}

reconsider p = f as Point of (TOP-REAL n) by A2, FUNCT_2:52;

len p = n by CARD_1:def 7;

then A4: dom p = Seg n by FINSEQ_1:def 3;

len ((Mx2Tran (Rotation (i,j,n,r))) . p) = n by CARD_1:def 7;

then A5: dom ((Mx2Tran (Rotation (i,j,n,r))) . p) = Seg n by FINSEQ_1:def 3;