theorem :: NEURONS1:11

for RNS1, RNS2 being RealLinearSpace st RLSStruct(# the carrier of RNS1, the ZeroF of RNS1, the addF of RNS1, the Mult of RNS1 #) = RLSStruct(# the carrier of RNS2, the ZeroF of RNS2, the addF of RNS2, the Mult of RNS2 #) holds
for F being set holds
( F is Function of RNS1,REAL iff F is Function of RNS2,REAL ) ;