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