thus ex f being Function of NAT ,F₁() st
( f . 0 = F₂() & ( for i being Nat holds f . (i + 1) = F₃(i,(f . i)) ) ) from NAT_1:sch 12(); :: thesis: for f1, f2 being Function of NAT ,F₁() st f1 . 0 = F₂() & ( for i being Nat holds f1 . (i + 1) = F₃(i,(f1 . i)) ) & f2 . 0 = F₂() & ( for i being Nat holds f2 . (i + 1) = F₃(i,(f2 . i)) ) holds
f1 = f2
let f1, f2 be Function of NAT ,F₁(); :: thesis: ( f1 . 0 = F₂() & ( for i being Nat holds f1 . (i + 1) = F₃(i,(f1 . i)) ) & f2 . 0 = F₂() & ( for i being Nat holds f2 . (i + 1) = F₃(i,(f2 . i)) ) implies f1 = f2 )
assume that
A1: f1 . 0 = F₂() and
B1: for i being Nat holds f1 . (i + 1) = F₃(i,(f1 . i)) and
A2: f2 . 0 = F₂() and
B2: for i being Nat holds f2 . (i + 1) = F₃(i,(f2 . i)) ; :: thesis: f1 = f2
thus f1 = f2 from NAT_1:sch 16(A1, B1, A2, B2); :: thesis: verum