thus ex f being sequence of 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 sequence of 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 sequence of 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
A2: for i being Nat holds f1 . (i + 1) = F₃(i,(f1 . i)) and
A3: f2 . 0 = F₂() and
A4: for i being Nat holds f2 . (i + 1) = F₃(i,(f2 . i)) ; :: thesis: f1 = f2
thus f1 = f2 from NAT_1:sch 16(A1, A2, A3, A4); :: thesis: verum