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