let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P _EQ_ (compell_ProjCo (z,p)) . Q iff (compell_ProjCo (z,p)) . P _EQ_ Q )
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P _EQ_ (compell_ProjCo (z,p)) . Q iff (compell_ProjCo (z,p)) . P _EQ_ Q )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P _EQ_ (compell_ProjCo (z,p)) . Q iff (compell_ProjCo (z,p)) . P _EQ_ Q )
set a = z `1 ;
set b = z `2 ;
set CP = (compell_ProjCo (z,p)) . P;
reconsider CP = (compell_ProjCo (z,p)) . P as Element of EC_SetProjCo ((z `1),(z `2),p) ;
set CQ = (compell_ProjCo (z,p)) . Q;
reconsider CQ = (compell_ProjCo (z,p)) . Q as Element of EC_SetProjCo ((z `1),(z `2),p) ;
hereby :: thesis: ( (compell_ProjCo (z,p)) . P _EQ_ Q implies P _EQ_ (compell_ProjCo (z,p)) . Q )
assume A1: P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ Q
(compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . CQ by A1, Th46;
hence (compell_ProjCo (z,p)) . P _EQ_ Q by Th41; :: thesis: verum
end;
assume A2: (compell_ProjCo (z,p)) . P _EQ_ Q ; :: thesis: P _EQ_ (compell_ProjCo (z,p)) . Q
(compell_ProjCo (z,p)) . CP _EQ_ (compell_ProjCo (z,p)) . Q by A2, Th46;
hence P _EQ_ (compell_ProjCo (z,p)) . Q by Th41; :: thesis: verum