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)

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

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

len (Base_FinSeq (n,i)) = n
by MATRIXR2:74;(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;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

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