let X be set ; :: thesis: for i, n being Nat
for f being additive homogeneous 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 i, n be Nat; :: thesis: for f being additive homogeneous 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 additive homogeneous 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 :: 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 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 TOPREAL3:46;
hence f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i) by A1, A3, Th33; :: thesis: verum