theorem Th30: :: MATRTOP3:30

for X being set
for k, n being Nat
for p being Point of (TOP-REAL n) st k in X & k in Seg n holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( 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 ) )