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