:: deftheorem defines ProjCo EC_PF_1:def 6 :
for K being Field holds ProjCo K = [: the carrier of K, the carrier of K, the carrier of K:] \ {[(0. K),(0. K),(0. K)]};