A3: for k being Nat
for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds
y1 = y2 by A2;
A4: for k being Nat
for y being set st 1 <= k & k < len F1() holds
ex z being set st P1[F1() . (k + 1),y,z] by A1;
thus ex x being set ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) from RECDEF_1:sch 5(A4); :: thesis: for x, y being set st ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds
x = y
let x, y be set ; :: thesis: ( ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) implies x = y )
assume A5: ex p being FinSequence st
( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ; :: thesis: ( for p being FinSequence holds
( not y = p . (len p) or not len p = len F1() or not p . 1 = F1() . 1 or ex k being Nat st
( 1 <= k & k < len F1() & P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) or x = y )
assume A6: ex p being FinSequence st
( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) ; :: thesis: x = y
thus x = y from RECDEF_1:sch 9(A3, A5, A6); :: thesis: verum