take the Isomorphism of R,S " ; :: thesis: ( the Isomorphism of R,S " is additive & the Isomorphism of R,S " is multiplicative & the Isomorphism of R,S " is unity-preserving & the Isomorphism of R,S " is isomorphism )
thus ( the Isomorphism of R,S " is additive & the Isomorphism of R,S " is multiplicative & the Isomorphism of R,S " is unity-preserving & the Isomorphism of R,S " is isomorphism ) by Lm7; :: thesis: verum