theorem :: PARSP_1:10

for F being Field holds the carrier of (MPS F) = [: the carrier of F, the carrier of F, the carrier of F:] ;