let n be Element of NAT ; :: thesis: 2 * (Lucas (n + 2)) = (Lucas n) + (Lucas (n + 3))
A1: (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3) by Th13;
thus 2 * (Lucas (n + 2)) = (Lucas (n + 2)) + (Lucas (n + 2))
.= ((Lucas (n + 1)) + (Lucas n)) + (Lucas (n + 2)) by Th12
.= (Lucas n) + (Lucas (n + 3)) by A1 ; :: thesis: verum