let X be set ; :: thesis: for i, n being Nat
for f being additive homogeneous rotation Function of (),() st f is X -support-yielding & not i in X holds
f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i)

let i, n be Nat; :: thesis: for f being additive homogeneous rotation Function of (),() st f is X -support-yielding & not i in X holds
f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i)

let f be additive homogeneous rotation Function of (),(); :: 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 :: thesis: for j being Nat st j in X /\ (Seg n) holds
(Base_FinSeq (n,i)) . j = 0
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 ;
hence (Base_FinSeq (n,i)) . j = 0 by ; :: thesis: verum
end;
len (Base_FinSeq (n,i)) = n by MATRIXR2:74;
then Base_FinSeq (n,i) is Point of () by TOPREAL3:46;
hence f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i) by A1, A3, Th33; :: thesis: verum