let p, q be Real; :: 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