theorem Th4: :: PARSP_1:4

for F being Field holds PRs F c= [:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:]