let n be non empty Element of NAT ; :: thesis: {((Fib n) * (Fib (n + 3))),((2 * (Fib (n + 1))) * (Fib (n + 2))),(((Fib (n + 1)) ^2 ) + ((Fib (n + 2)) ^2 ))} is Pythagorean_triple
(((Fib n) * (Fib (n + 3))) ^2 ) + (((2 * (Fib (n + 1))) * (Fib (n + 2))) ^2 ) = (((Fib n) ^2 ) * ((Fib (n + 3)) ^2 )) + (((2 * 2) * ((Fib (n + 1)) ^2 )) * ((Fib (n + 2)) ^2 ))
.= (((Fib n) ^2 ) * (((Fib (n + 2)) + (Fib (n + 1))) ^2 )) + ((4 * ((Fib (n + 1)) ^2 )) * ((Fib (n + 2)) ^2 )) by Th27
.= ((((Fib (n + 2)) - (Fib (n + 1))) ^2 ) * (((Fib (n + 2)) + (Fib (n + 1))) ^2 )) + ((4 * ((Fib (n + 1)) ^2 )) * ((Fib (n + 2)) ^2 )) by Th32
.= (((Fib (n + 1)) ^2 ) + ((Fib (n + 2)) ^2 )) ^2 ;
hence {((Fib n) * (Fib (n + 3))),((2 * (Fib (n + 1))) * (Fib (n + 2))),(((Fib (n + 1)) ^2 ) + ((Fib (n + 2)) ^2 ))} is Pythagorean_triple by PYTHTRIP:def 4; :: thesis: verum