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