let X be set ; :: thesis:
let k, n be Nat; :: thesis:
let p be Point of (TOP-REAL n); :: thesis:
assume that
A1: k in X and
A2: k in Seg n ; :: thesis:
set TR = TOP-REAL n;
defpred S₁[ Nat] means ( $1 <= n implies ex f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) st
( f is (X /\ (Seg $1)) \/ {k} -support-yielding & ( card ((X /\ (Seg $1)) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg $1) & i <> k holds
(f . p) . i = 0 ) ) );
A3: for z being Nat st S₁[z] holds
S₁[z + 1]

let z be Nat; :: thesis:
set z1 = z + 1;
assume A4: S₁[z] ; :: thesis:
A5: Seg (z + 1) = (Seg z) \/ {(z + 1)} by FINSEQ_1:9;
A6: Seg (z + 1) = (Seg z) \/ {(z + 1)} by FINSEQ_1:9;
A7: ( z + 1 in X implies ((X /\ (Seg z)) \/ {k}) \/ {(z + 1),k} = (X /\ (Seg (z + 1))) \/ {k} )

assume z + 1 in X ; :: thesis:
then A8: X \/ {(z + 1)} = X by ZFMISC_1:40;
{(z + 1),k} = {(z + 1)} \/ {k} by ENUMSET1:1;
hence ((X /\ (Seg z)) \/ {k}) \/ {(z + 1),k} = (X /\ (Seg z)) \/ ({k} \/ ({k} \/ {(z + 1)})) by XBOOLE_1:4
.= (X /\ (Seg z)) \/ (({k} \/ {k}) \/ {(z + 1)}) by XBOOLE_1:4
.= ((X /\ (Seg z)) \/ {(z + 1)}) \/ {k} by XBOOLE_1:4
.= (X /\ (Seg (z + 1))) \/ {k} by A6, A8, XBOOLE_1:24 ;
:: thesis:

end;

assume A9: z + 1 <= n ; :: thesis:
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A10: f is (X /\ (Seg z)) \/ {k} -support-yielding and
A11: ( card ((X /\ (Seg z)) \/ {k}) > 1 implies (f . p) . k >= 0 ) and
A12: for m being Nat st m in X /\ (Seg z) & m <> k holds
(f . p) . m = 0 by A4, NAT_1:13;
set z1 = z + 1;

per cases by XXREAL_0:1;

suppose A13: z + 1 = k ; :: thesis:

take f ; :: thesis:
(Seg (z + 1)) \/ {(z + 1)} = (Seg z) \/ ({(z + 1)} \/ {(z + 1)}) by A5, XBOOLE_1:4
.= (Seg z) \/ {(z + 1)} ;
then A14: (X /\ (Seg (z + 1))) \/ {k} = (X \/ {k}) /\ ((Seg z) \/ {k}) by A13, XBOOLE_1:24
.= (X /\ (Seg z)) \/ {k} by XBOOLE_1:24 ;
hence f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding by A10; :: thesis:
thus ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) by A11, A14; :: thesis:
let m be Nat; :: thesis:
assume that
A15: m in X /\ (Seg (z + 1)) and
A16: m <> k ; :: thesis:
A17: m in Seg (z + 1) by A15, XBOOLE_0:def 4;
A18: m in X by A15, XBOOLE_0:def 4;
not m in {(z + 1)} by A13, A16, TARSKI:def 1;
then m in Seg z by A5, A17, XBOOLE_0:def 3;
then m in X /\ (Seg z) by A18, XBOOLE_0:def 4;
hence (f . p) . m = 0 by A12, A16; :: thesis:

end;

suppose A19: not z + 1 in X ; :: thesis:

take f ; :: thesis:
A20: {(z + 1)} misses X by A19, ZFMISC_1:50;
A21: X /\ (Seg (z + 1)) = (X /\ (Seg z)) \/ (X /\ {(z + 1)}) by A5, XBOOLE_1:23
.= (X /\ (Seg z)) \/ {} by A20, XBOOLE_0:def 7
.= X /\ (Seg z) ;
hence f is (X /\ (Seg (z + 1))) \/ {k} -support-yielding by A10; :: thesis:
thus ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (f . p) . k >= 0 ) by A11, A21; :: thesis:
let m be Nat; :: thesis:
assume that
A22: m in X /\ (Seg (z + 1)) and
A23: m <> k ; :: thesis:
A24: m in Seg (z + 1) by A22, XBOOLE_0:def 4;
A25: m in X by A22, XBOOLE_0:def 4;
then not m in {(z + 1)} by A19, TARSKI:def 1;
then m in Seg z by A5, A24, XBOOLE_0:def 3;
then m in X /\ (Seg z) by A25, XBOOLE_0:def 4;
hence (f . p) . m = 0 by A12, A23; :: thesis:

end;

suppose A26: ( z + 1 < k & z + 1 in X ) ; :: thesis:

set fp = f . p;
set S = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2);
A27: ( z + 1 >= 1 & k <= n ) by A2, FINSEQ_1:1, NAT_1:11;
A28: ( ((f . p) . k) ^2 >= 0 & ((f . p) . (z + 1)) ^2 >= 0 ) by XREAL_1:63;
then A29: (sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2))) ^2 = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2) by SQUARE_1:def 2;
then consider r being Real such that
A30: ((Mx2Tran (Rotation ((z + 1),k,n,r))) . (f . p)) . k = sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2)) by A26, A27, Th25;
reconsider M = Mx2Tran (Rotation ((z + 1),k,n,r)) as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A26, A27, Th28;
take Mf = M * f; :: thesis:
A31: M is {(z + 1),k} -support-yielding by A26, A27, Th26;
hence Mf is (X /\ (Seg (z + 1))) \/ {k} -support-yielding by A7, A10, A26; :: thesis:
A32: dom Mf = the carrier of (TOP-REAL n) by FUNCT_2:52;
then A33: f . p in dom M by FUNCT_1:11;
A34: Mf . p = M . (f . p) by A32, FUNCT_1:12;
hence ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (Mf . p) . k >= 0 ) by A28, A30, SQUARE_1:def 2; :: thesis:
let i be Nat; :: thesis:
assume that
A35: i in X /\ (Seg (z + 1)) and
A36: i <> k ; :: thesis:
A37: i in X by A35, XBOOLE_0:def 4;
i in Seg (z + 1) by A35, XBOOLE_0:def 4;
then A38: ( i in Seg z or i in {(z + 1)} ) by A5, XBOOLE_0:def 3;

per cases by A38, TARSKI:def 1;

suppose A39: i in Seg z ; :: thesis:

then A40: i in X /\ (Seg z) by A37, XBOOLE_0:def 4;
i <= z by A39, FINSEQ_1:1;
then i < z + 1 by NAT_1:13;
then not i in {(z + 1),k} by A36, TARSKI:def 2;
hence (Mf . p) . i = (f . p) . i by A31, A33, A34
.= 0 by A12, A36, A40 ;
:: thesis:

end;

suppose i = z + 1 ; :: thesis:

then A41: (((M . (f . p)) . i) * ((M . (f . p)) . i)) + ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2)) = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2) by A26, A27, A29, A30, Lm6;
thus (Mf . p) . i = (M . (f . p)) . i by A32, FUNCT_1:12
.= 0 by A41 ; :: thesis:

end;

suppose A42: ( z + 1 > k & z + 1 in X ) ; :: thesis:

set fp = f . p;
set S = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2);
A43: 1 <= k by A2, FINSEQ_1:1;
A44: ( ((f . p) . k) ^2 >= 0 & ((f . p) . (z + 1)) ^2 >= 0 ) by XREAL_1:63;
then A45: (sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2))) ^2 = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2) by SQUARE_1:def 2;
then consider r being Real such that
A46: ((Mx2Tran (Rotation (k,(z + 1),n,r))) . (f . p)) . k = sqrt ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2)) by A9, A42, A43, Th24;
reconsider M = Mx2Tran (Rotation (k,(z + 1),n,r)) as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A9, A42, A43, Th28;
take Mf = M * f; :: thesis:
A47: M is {k,(z + 1)} -support-yielding by A9, A42, A43, Th26;
hence Mf is (X /\ (Seg (z + 1))) \/ {k} -support-yielding by A7, A10, A42; :: thesis:
A48: dom Mf = the carrier of (TOP-REAL n) by FUNCT_2:52;
then A49: Mf . p = M . (f . p) by FUNCT_1:12;
hence ( card ((X /\ (Seg (z + 1))) \/ {k}) > 1 implies (Mf . p) . k >= 0 ) by A44, A46, SQUARE_1:def 2; :: thesis:
let i be Nat; :: thesis:
assume that
A50: i in X /\ (Seg (z + 1)) and
A51: i <> k ; :: thesis:
A52: i in X by A50, XBOOLE_0:def 4;
i in Seg (z + 1) by A50, XBOOLE_0:def 4;
then A53: ( i in Seg z or i in {(z + 1)} ) by A5, XBOOLE_0:def 3;

per cases by A53, TARSKI:def 1;

suppose A54: i in Seg z ; :: thesis:

then i <= z by FINSEQ_1:1;
then i < z + 1 by NAT_1:13;
then A55: not i in {(z + 1),k} by A51, TARSKI:def 2;
A56: i in X /\ (Seg z) by A52, A54, XBOOLE_0:def 4;
f . p in dom M by A48, FUNCT_1:11;
hence (Mf . p) . i = (f . p) . i by A47, A49, A55
.= 0 by A12, A51, A56 ;
:: thesis:

end;

suppose i = z + 1 ; :: thesis:

then A57: (((M . (f . p)) . i) * ((M . (f . p)) . i)) + ((((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2)) = (((f . p) . (z + 1)) ^2) + (((f . p) . k) ^2) by A9, A42, A43, A45, A46, Lm6;
thus (Mf . p) . i = (M . (f . p)) . i by A48, FUNCT_1:12
.= 0 by A57 ; :: thesis:

end;

A58: S₁[ 0 ]

proof

assume 0 <= n ; :: thesis:
take f = id (TOP-REAL n); :: thesis:
A59: f is {} -support-yielding by FUNCT_1:17;
thus f is (X /\ (Seg 0)) \/ {k} -support-yielding by A59; :: thesis:
thus ( card ((X /\ (Seg 0)) \/ {k}) > 1 implies (f . p) . k >= 0 ) by CARD_2:42; :: thesis:
let m be Nat; :: thesis:
assume m in X /\ (Seg 0) ; :: thesis:
hence ( not m <> k or (f . p) . m = 0 ) ; :: thesis:

end;

for z being Nat holds S₁[z] from NAT_1:sch 2(A58, A3);
then consider f being base_rotation Function of (TOP-REAL n),(TOP-REAL n) such that
A60: ( f is (X /\ (Seg n)) \/ {k} -support-yielding & ( card ((X /\ (Seg n)) \/ {k}) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) ) ;
take f ; :: thesis:
A61: X /\ (Seg n) c= X by XBOOLE_1:17;
( {k} c= X & {k} c= Seg n ) by A1, A2, ZFMISC_1:31;
then (X /\ (Seg n)) \/ {k} = X /\ (Seg n) by XBOOLE_1:12, XBOOLE_1:19;
hence ( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds
(f . p) . i = 0 ) ) by A60, A61; :: thesis: