let p, q be Real; :: 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) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (sinh . (p + (- q))) by Lm3
.= (((sinh . p) * (cosh . q)) + ((cosh . p) * (sinh . q))) * (((sinh . p) * (cosh . (- q))) + ((cosh . p) * (sinh . (- q)))) by Lm3
.= (((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)) ;
then A2: (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))))
.= (((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) ;
(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)) & (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