theorem :: PARSP_1:1

for F being Field
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by Def1;