let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = P
let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = P
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = P
set Q = (compell_ProjCo (z,p)) . P;
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),(P `3_3)] by Def8;
then A1: ( ((compell_ProjCo (z,p)) . P) `1_3 = P `1_3 & ((compell_ProjCo (z,p)) . P) `2_3 = - (P `2_3) & ((compell_ProjCo (z,p)) . P) `3_3 = P `3_3 ) by Def3, Def4, Def5;
set R = (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P);
(compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = [(((compell_ProjCo (z,p)) . P) `1_3),(- (((compell_ProjCo (z,p)) . P) `2_3)),(((compell_ProjCo (z,p)) . P) `3_3)] by Def8;
then ( ((compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P)) `1_3 = P `1_3 & ((compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P)) `2_3 = - (- (P `2_3)) & ((compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P)) `3_3 = P `3_3 ) by A1, Def3, Def4, Def5;
then ( ((compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P)) `1_3 = P `1_3 & ((compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P)) `2_3 = P `2_3 & ((compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P)) `3_3 = P `3_3 ) by RLVECT_1:17;
then (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = [(P `1_3),(P `2_3),(P `3_3)] by Th31;
hence (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = P by Th31; :: thesis: verum