theorem Th30: :: LOPBAN14:29

for X, Y being RealLinearSpace-Sequence holds carr (X ^ Y) = (carr X) ^ (carr Y)