theorem Th25: :: HILB10_1:22

for x, y being Integer
for a being non trivial Nat holds
( Px (a,|.(x + y).|) = ((Px (a,|.x.|)) * (Px (a,|.y.|))) + ((((((a ^2) -' 1) * (sgn x)) * (Py (a,|.x.|))) * (sgn y)) * (Py (a,|.y.|))) & (sgn (x + y)) * (Py (a,|.(x + y).|)) = (((Px (a,|.x.|)) * (sgn y)) * (Py (a,|.y.|))) + (((sgn x) * (Py (a,|.x.|))) * (Px (a,|.y.|))) )