let X be set ; :: thesis: for n being Nat
for p being Point of (TOP-REAL n)
for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds
p . i = 0 ) holds
f . p = p
let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds
p . i = 0 ) holds
f . p = p
let p be Point of (TOP-REAL n); :: thesis: for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds
p . i = 0 ) holds
f . p = p
set TR = TOP-REAL n;
let f be rotation Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds
p . i = 0 ) implies f . p = p )
assume that
A1: f is X -support-yielding and
A2: for i being Nat st i in X /\ (Seg n) holds
p . i = 0 ; :: thesis: f . p = p
set sp = sqr p;
set sfp = sqr (f . p);
A3: Sum (sqr p) >= 0 by RVSUM_1:86;
( Sum (sqr (f . p)) >= 0 & |.(f . p).| = |.p.| ) by Def4, RVSUM_1:86;
then A4: Sum (sqr p) = Sum (sqr (f . p)) by A3, SQUARE_1:28;
A5: len p = n by CARD_1:def 7;
p = @ (@ p) ;
then A6: len (sqr p) = n by A5, TOPREAL7:8;
A7: len (f . p) = n by CARD_1:def 7;
@ (@ (f . p)) = f . p ;
then len (sqr (f . p)) = n by A7, TOPREAL7:8;
then reconsider sp = sqr p, sfp = sqr (f . p) as Element of n -tuples_on REAL by A6, FINSEQ_2:92;
A8: dom f = the carrier of (TOP-REAL n) by FUNCT_2:52;
A9: for i being Nat st i in Seg n holds
sp . i <= sfp . i

proof

let i be Nat; :: thesis: ( i in Seg n implies sp . i <= sfp . i )
A10: ( sp . i = (p . i) ^2 & sfp . i = ((f . p) . i) ^2 ) by VALUED_1:11;
assume A11: i in Seg n ; :: thesis: sp . i <= sfp . i

per cases ( i in X or not i in X ) ;

suppose i in X ; :: thesis: sp . i <= sfp . i

then i in X /\ (Seg n) by A11, XBOOLE_0:def 4;
then p . i = 0 by A2;
hence sp . i <= sfp . i by A10, XREAL_1:63; :: thesis: verum

end;

suppose not i in X ; :: thesis: sp . i <= sfp . i

hence sp . i <= sfp . i by A1, A8, A10, Def1; :: thesis: verum

end;

end;

end;

for i being Nat st 1 <= i & i <= n holds
p . i = (f . p) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= n implies p . i = (f . p) . i )
A12: sp . i = (p . i) ^2 by VALUED_1:11;
assume ( 1 <= i & i <= n ) ; :: thesis: p . i = (f . p) . i
then A13: i in Seg n by FINSEQ_1:1;
then A14: ( sp . i >= sfp . i & sp . i <= sfp . i ) by A4, A9, RVSUM_1:83;

per cases ( i in X or not i in X ) ;

suppose i in X ; :: thesis: p . i = (f . p) . i

then A15: i in X /\ (Seg n) by A13, XBOOLE_0:def 4;
then p . i = 0 by A2;
then ((f . p) . i) ^2 = 0 by A12, A14, VALUED_1:11;
then (f . p) . i = 0 ;
hence p . i = (f . p) . i by A2, A15; :: thesis: verum

end;

suppose not i in X ; :: thesis: p . i = (f . p) . i

hence p . i = (f . p) . i by A1, A8, Def1; :: thesis: verum

end;

end;

end;

hence f . p = p by A5, A7, FINSEQ_1:14; :: thesis: verum