defpred S1[ Nat, set , set ] means P1[F1() . ($1 + 1),$2,$3];
A2:
for k being Nat st 1 <= k & k < len F1() holds
for x being set ex y being set st S1[k,x,y]
by A1;
consider p being FinSequence such that
A3:
( len p = len F1() & ( p . 1 = F1() . 1 or len F1() = 0 ) & ( for k being Nat st 1 <= k & k < len F1() holds
S1[k,p . k,p . (k + 1)] ) )
from RECDEF_1:sch 3(A2);
A4:
( len F1() <> 0 implies 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)] ) ) )
proof
assume A5:
len F1()
<> 0
;
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)] ) )
take
p . (len p)
;
ex p being FinSequence st
( p . (len p) = 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)] ) )
take
p
;
( p . (len p) = 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)] ) )
thus
(
p . (len p) = p . (len p) &
len p = len F1() &
p . 1
= F1()
. 1 )
by A3, A5;
for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)]
let k be
Nat;
( 1 <= k & k < len F1() implies P1[F1() . (k + 1),p . k,p . (k + 1)] )
assume
( 1
<= k &
k < len F1() )
;
P1[F1() . (k + 1),p . k,p . (k + 1)]
hence
P1[
F1()
. (k + 1),
p . k,
p . (k + 1)]
by A3;
verum
end;
( len F1() = 0 implies 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)] ) ) )
proof
assume A6:
len F1()
= 0
;
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)] ) )
take
F1()
. 0
;
ex p being FinSequence st
( F1() . 0 = 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)] ) )
take
F1()
;
( F1() . 0 = F1() . (len F1()) & len F1() = len F1() & F1() . 1 = F1() . 1 & ( for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),F1() . k,F1() . (k + 1)] ) )
thus
(
F1()
. 0 = F1()
. (len F1()) &
len F1()
= len F1() &
F1()
. 1
= F1()
. 1 )
by A6;
for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),F1() . k,F1() . (k + 1)]
thus
for
k being
Nat st 1
<= k &
k < len F1() holds
P1[
F1()
. (k + 1),
F1()
. k,
F1()
. (k + 1)]
by A6;
verum
end;
hence
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)] ) )
by A4; verum