let X be set ; :: thesis: for n, i being Nat
for f being homogeneous additive rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & not i in X holds
f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i)
let n, i be Nat; :: thesis: for f being homogeneous additive rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & not i in X holds
f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i)
let f be homogeneous additive rotation Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is X -support-yielding & not i in X implies f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i) )
set B = Base_FinSeq (n,i);
assume that
A1: f is X -support-yielding and
A2: not i in X ; :: thesis: f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i)

A3: now

let j be Nat; :: thesis: ( j in X /\ (Seg n) implies (Base_FinSeq (n,i)) . j = 0 )
assume A4: j in X /\ (Seg n) ; :: thesis: (Base_FinSeq (n,i)) . j = 0
then j in Seg n by XBOOLE_0:def 4;
then A5: ( 1 <= j & j <= n ) by FINSEQ_1:1;
j <> i by A2, A4, XBOOLE_0:def 4;
hence (Base_FinSeq (n,i)) . j = 0 by A5, MATRIXR2:76; :: thesis: verum

end;

len (Base_FinSeq (n,i)) = n by MATRIXR2:74;
then Base_FinSeq (n,i) is Point of (TOP-REAL n) by TOPREAL7:17;
hence f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i) by A1, A3, Th32; :: thesis: verum