A2:
for n being Nat st 1 <= n & n < size holds
for x being Element of PFuncs ((ND (V,A)),(ND (V,A))) ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S1[n,x,y]
proof
let n be
Nat;
( 1 <= n & n < size implies for x being Element of PFuncs ((ND (V,A)),(ND (V,A))) ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S1[n,x,y] )
assume
( 1
<= n &
n < size )
;
for x being Element of PFuncs ((ND (V,A)),(ND (V,A))) ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S1[n,x,y]
let x be
Element of
PFuncs (
(ND (V,A)),
(ND (V,A)));
ex y being Element of PFuncs ((ND (V,A)),(ND (V,A))) st S1[n,x,y]
reconsider f =
x as
PartFunc of
(ND (V,A)),
(ND (V,A)) by PARTFUN1:46;
reconsider y =
PP_composition (
f,
(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) as
Element of
PFuncs (
(ND (V,A)),
(ND (V,A)))
by PARTFUN1:45;
take
y
;
S1[n,x,y]
thus
S1[
n,
x,
y]
;
verum
end;
consider F being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) such that
A3:
len F = size
and
A4:
( F . 1 = X or size = 0 )
and
A5:
for n being Nat st 1 <= n & n < size holds
S1[n,F . n,F . (n + 1)]
from RECDEF_1:sch 4(A2);
take
F
; ( len F = size & F . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds
F . (n + 1) = PP_composition ((F . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) )
thus
len F = size
by A3; ( F . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds
F . (n + 1) = PP_composition ((F . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) )
thus
F . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))
by A1, A4; for n being Nat st 1 <= n & n < size holds
F . (n + 1) = PP_composition ((F . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1)))))
let n be Nat; ( 1 <= n & n < size implies F . (n + 1) = PP_composition ((F . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) )
assume
( 1 <= n & n < size )
; F . (n + 1) = PP_composition ((F . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1)))))
then
S1[n,F . n,F . (n + 1)]
by A5;
hence
F . (n + 1) = PP_composition ((F . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1)))))
; verum