let p, q be real number ; :: thesis: ( ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = (sinh . (p + q)) * (sinh . (p - q)) & (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) & ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) )
A1: (sinh . (p + q)) * (sinh . (p - q)) = (((sinh . p) ^2 ) * ((cosh . q) ^2 )) - (((sinh . q) ^2 ) * ((cosh . p) ^2 ))

proof

(sinh . (p + q)) * (sinh . (p - q)) = (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (sinh . (p + (- q))) by Lm4
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . (- q))) + ((cosh . p) * (sinh . (- q)))) by Lm4
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . (- q)))) by Th19
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . q)) + ((cosh . p) * (- (sinh . q)))) by Th19
.= (((sinh . p) ^2 ) * ((cosh . q) ^2 )) - (((sinh . q) ^2 ) * ((cosh . p) ^2 )) ;
hence (sinh . (p + q)) * (sinh . (p - q)) = (((sinh . p) ^2 ) * ((cosh . q) ^2 )) - (((sinh . q) ^2 ) * ((cosh . p) ^2 )) ; :: thesis: verum

end;

A2: ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = (sinh . (p + q)) * (sinh . (p - q))

proof

(sinh . (p + q)) * (sinh . (p - q)) = ((((sinh . p) ^2 ) * (((cosh . q) ^2 ) - ((sinh . q) ^2 ))) + (((sinh . q) ^2 ) * ((sinh . p) ^2 ))) - (((sinh . q) ^2 ) * ((cosh . p) ^2 )) by A1
.= ((((sinh . p) ^2 ) * 1) + (((sinh . p) ^2 ) * ((sinh . q) ^2 ))) - (((sinh . q) ^2 ) * ((cosh . p) ^2 )) by Th14
.= ((sinh . p) ^2 ) + (((sinh . q) ^2 ) * (- (((cosh . p) ^2 ) - ((sinh . p) ^2 ))))
.= ((sinh . p) ^2 ) + (((sinh . q) ^2 ) * (- 1)) by Th14
.= ((sinh . p) ^2 ) - ((sinh . q) ^2 ) ;
hence ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = (sinh . (p + q)) * (sinh . (p - q)) ; :: thesis: verum

end;

(sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2 ) - ((cosh . q) ^2 )

proof

(sinh . (p + q)) * (sinh . (p - q)) = (((cosh . q) ^2 ) * (- (((cosh . p) ^2 ) - ((sinh . p) ^2 )))) + ((((cosh . p) ^2 ) * ((cosh . q) ^2 )) + (- (((sinh . q) ^2 ) * ((cosh . p) ^2 )))) by A1
.= (((cosh . q) ^2 ) * (- 1)) + (((cosh . p) ^2 ) * (((cosh . q) ^2 ) - ((sinh . q) ^2 ))) by Th14
.= (((cosh . q) ^2 ) * (- 1)) + (((cosh . p) ^2 ) * 1) by Th14
.= ((cosh . p) ^2 ) - ((cosh . q) ^2 ) ;
hence (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) ; :: thesis: verum

end;

hence ( ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = (sinh . (p + q)) * (sinh . (p - q)) & (sinh . (p + q)) * (sinh . (p - q)) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) & ((sinh . p) ^2 ) - ((sinh . q) ^2 ) = ((cosh . p) ^2 ) - ((cosh . q) ^2 ) ) by A2; :: thesis: verum