let p, q be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( ^ (p + q) = (^ p) + (^ q) & ^ (p * q) = (^ p) * (^ q) )
A3: ^ (p + q) = ~ (p + q)
.= (~ p) + (~ q) by POLYNOM3:def 10
.= (~ (^ p)) + (~ (^ q)) by FIELD_4:15
.= ~ ((^ p) + (^ q)) by POLYNOM3:def 10
.= (^ p) + (^ q) ;
^ (p * q) = ~ (p * q)
.= (~ p) *' (~ q) by POLYNOM3:def 10
.= (~ (^ p)) *' (~ (^ q)) by FIELD_4:17
.= ~ ((^ p) * (^ q)) by POLYNOM3:def 10
.= (^ p) * (^ q) ;
hence ( ^ (p + q) = (^ p) + (^ q) & ^ (p * q) = (^ p) * (^ q) ) by A3; :: thesis: verum