set L = Lucas ;
A1: Lucas . 0 = [2,1] by Def1;
thus Lucas 0 = [2,1] `1 by Def1
.= 2 ; :: thesis: ( Lucas 1 = 1 & ( for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1)) ) )
thus Lucas 1 = (Lucas . (0 + 1)) `1
.= [((Lucas . 0) `2),(((Lucas . 0) `1) + ((Lucas . 0) `2))] `1 by Def1
.= 1 by A1 ; :: thesis: for n being Nat holds Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1))
let n be Nat; :: thesis: Lucas ((n + 1) + 1) = (Lucas n) + (Lucas (n + 1))
A3: (Lucas . (n + 1)) `1 = [((Lucas . n) `2),(((Lucas . n) `1) + ((Lucas . n) `2))] `1 by Def1
.= (Lucas . n) `2 ;
thus Lucas ((n + 1) + 1) = [((Lucas . (n + 1)) `2),(((Lucas . (n + 1)) `1) + ((Lucas . (n + 1)) `2))] `1 by Def1
.= [((Lucas . n) `2),(((Lucas . n) `1) + ((Lucas . n) `2))] `2 by Def1
.= (Lucas n) + (Lucas (n + 1)) by A3 ; :: thesis: verum