let n be non zero 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 Th25
.= ((((Fib (n + 2)) - (Fib (n + 1))) ^2) * (((Fib (n + 2)) + (Fib (n + 1))) ^2)) + ((4 * ((Fib (n + 1)) ^2)) * ((Fib (n + 2)) ^2)) by Th30
.= (((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