for n being non empty Nat
for At being Subset of (TOP-REAL n)
for Ar being Subset of (n -VectSp_over F_Real) st At = Ar holds
( the carrier of (Lin At) = the carrier of (Lin Ar) & 0. (Lin At) = 0. (Lin Ar) & the addF of (Lin At) = the addF of (Lin Ar) & the Mult of (Lin At) = the lmult of (Lin Ar) )