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 ; :: thesis: 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) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: for k being Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)]
let k be Nat; :: thesis: ( 1 <= k & k < len F1() implies P1[F1() . (k + 1),p . k,p . (k + 1)] )
assume ( 1 <= k & k < len F1() ) ; :: thesis: P1[F1() . (k + 1),p . k,p . (k + 1)]
hence P1[F1() . (k + 1),p . k,p . (k + 1)] by A3; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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() ; :: thesis: ( 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; :: thesis: 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; :: thesis: 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; :: thesis: verum