let p, q be real number ; :: thesis: ( ((sinh . p) ^2 ) + ((cosh . q) ^2 ) = (cosh . (p + q)) * (cosh . (p - q)) & (cosh . (p + q)) * (cosh . (p - q)) = ((cosh . p) ^2 ) + ((sinh . q) ^2 ) & ((sinh . p) ^2 ) + ((cosh . q) ^2 ) = ((cosh . p) ^2 ) + ((sinh . q) ^2 ) )
A1: (cosh . (p + q)) * (cosh . (p - q)) = (((cosh . p) * (cosh . q)) + ((sinh . p) * (sinh . q))) * (cosh . (p + (- q))) by Lm2
.= (((cosh . p) * (cosh . q)) + ((sinh . p) * (sinh . q))) * (((cosh . p) * (cosh . (- q))) + ((sinh . p) * (sinh . (- q)))) by Lm2
.= (((((cosh . p) * (cosh . q)) * ((cosh . p) * (cosh . (- q)))) + (((cosh . p) * (cosh . q)) * ((sinh . p) * (sinh . (- q))))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . (- q))))) + (((sinh . p) * (sinh . q)) * ((sinh . p) * (sinh . (- q))))
.= (((((cosh . p) * (cosh . q)) * ((cosh . p) * (cosh . q))) + (((cosh . p) * (cosh . q)) * ((sinh . (- q)) * (sinh . p)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . (- q))))) + (((sinh . p) * (sinh . q)) * ((sinh . (- q)) * (sinh . p))) by Th19
.= (((((cosh . p) * (cosh . q)) ^2 ) + (((sinh . (- q)) * (sinh . p)) * ((cosh . p) * (cosh . q)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . q)))) + (((sinh . (- q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19
.= (((((cosh . p) * (cosh . q)) ^2 ) + (((- (sinh . q)) * (sinh . p)) * ((cosh . p) * (cosh . q)))) + (((sinh . p) * (sinh . q)) * ((cosh . p) * (cosh . q)))) + (((sinh . (- q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19
.= ((((cosh . p) * (cosh . q)) ^2 ) + 0 ) + ((((- 1) * (sinh . q)) * (sinh . p)) * ((sinh . p) * (sinh . q))) by Th19
.= (((cosh . p) ^2 ) * ((cosh . q) ^2 )) - (((sinh . q) ^2 ) * ((sinh . p) ^2 )) ;
then A2: (cosh . (p + q)) * (cosh . (p - q)) = ((((cosh . p) ^2 ) * (((cosh . q) ^2 ) - ((sinh . q) ^2 ))) + (((cosh . p) ^2 ) * ((sinh . q) ^2 ))) + (- (((sinh . q) ^2 ) * ((sinh . p) ^2 )))
.= ((((cosh . p) ^2 ) * 1) + (((cosh . p) ^2 ) * ((sinh . q) ^2 ))) + (- (((sinh . q) ^2 ) * ((sinh . p) ^2 ))) by Th14
.= ((cosh . p) ^2 ) + (((sinh . q) ^2 ) * (((cosh . p) ^2 ) - ((sinh . p) ^2 )))
.= ((cosh . p) ^2 ) + (((sinh . q) ^2 ) * 1) by Th14
.= ((cosh . p) ^2 ) + ((sinh . q) ^2 ) ;
(cosh . (p + q)) * (cosh . (p - q)) = (((cosh . q) ^2 ) * (((cosh . p) ^2 ) - ((sinh . p) ^2 ))) + ((((cosh . q) ^2 ) * ((sinh . p) ^2 )) + (- (((sinh . p) ^2 ) * ((sinh . q) ^2 )))) by A1
.= (((cosh . q) ^2 ) * 1) + ((((cosh . q) ^2 ) * ((sinh . p) ^2 )) - (((sinh . p) ^2 ) * ((sinh . q) ^2 ))) by Th14
.= ((cosh . q) ^2 ) + (((sinh . p) ^2 ) * (((cosh . q) ^2 ) - ((sinh . q) ^2 )))
.= ((cosh . q) ^2 ) + (((sinh . p) ^2 ) * 1) by Th14
.= ((cosh . q) ^2 ) + ((sinh . p) ^2 ) ;
hence ( ((sinh . p) ^2 ) + ((cosh . q) ^2 ) = (cosh . (p + q)) * (cosh . (p - q)) & (cosh . (p + q)) * (cosh . (p - q)) = ((cosh . p) ^2 ) + ((sinh . q) ^2 ) & ((sinh . p) ^2 ) + ((cosh . q) ^2 ) = ((cosh . p) ^2 ) + ((sinh . q) ^2 ) ) by A2; :: thesis: verum