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;

then A6: len (sqr p) = n by RVSUM_1:143;

A7: len (f . p) = n by CARD_1:def 7;

then len (sqr (f . p)) = n by RVSUM_1:143;

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

p . i = (f . p) . i

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;

then A6: len (sqr p) = n by RVSUM_1:143;

A7: len (f . p) = n by CARD_1:def 7;

then len (sqr (f . p)) = n by RVSUM_1:143;

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

for i being Nat st 1 <= i & i <= n holds
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

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

p . i = (f . p) . i

proof

hence
f . p = p
by A5, A7; :: thesis: verum
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 ;

then A14: ( sp . i >= sfp . i & sp . i <= sfp . i ) by A4, A9, RVSUM_1:83;

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

then A14: ( sp . i >= sfp . i & sp . i <= sfp . i ) by A4, A9, RVSUM_1:83;