let i, n be Nat; :: thesis: ( i in Seg n implies Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding )

set M = Mx2Tran (AxialSymmetry (i,n));

assume A1: i in Seg n ; :: thesis: Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding

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

x in {i}

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

assume f in dom (Mx2Tran (AxialSymmetry (i,n))) ; :: thesis: ( not ((Mx2Tran (AxialSymmetry (i,n))) . f) . x <> f . x or x in {i} )

then reconsider F = f as Point of (TOP-REAL n) by FUNCT_2:52;

assume A2: ((Mx2Tran (AxialSymmetry (i,n))) . f) . x <> f . x ; :: thesis: x in {i}

len ((Mx2Tran (AxialSymmetry (i,n))) . F) = n by CARD_1:def 7;

then A3: dom ((Mx2Tran (AxialSymmetry (i,n))) . F) = Seg n by FINSEQ_1:def 3;

A4: len F = n by CARD_1:def 7;

then A5: dom F = Seg n by FINSEQ_1:def 3;

set M = Mx2Tran (AxialSymmetry (i,n));

assume A1: i in Seg n ; :: thesis: Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding

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

x in {i}

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

assume f in dom (Mx2Tran (AxialSymmetry (i,n))) ; :: thesis: ( not ((Mx2Tran (AxialSymmetry (i,n))) . f) . x <> f . x or x in {i} )

then reconsider F = f as Point of (TOP-REAL n) by FUNCT_2:52;

assume A2: ((Mx2Tran (AxialSymmetry (i,n))) . f) . x <> f . x ; :: thesis: x in {i}

len ((Mx2Tran (AxialSymmetry (i,n))) . F) = n by CARD_1:def 7;

then A3: dom ((Mx2Tran (AxialSymmetry (i,n))) . F) = Seg n by FINSEQ_1:def 3;

A4: len F = n by CARD_1:def 7;

then A5: dom F = Seg n by FINSEQ_1:def 3;