theorem Th77: :: REAL_NS2:77

for T being RealLinearSpace
for Af being Subset of (RLSp2RVSp T)
for Ar being Subset of T st Af = Ar holds
[#] (Lin Ar) = [#] (Lin Af)