let n be Element of NAT ; :: thesis: (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))
A1: 2 * (GenFib (2,1,(n + 2))) = 2 * (Lucas (n + 2)) by Th38;
( GenFib (2,1,n) = Lucas n & GenFib (2,1,(n + 3)) = Lucas (n + 3) ) by Th38;
hence (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2)) by A1, Th39; :: thesis: verum