let F be Subset of PL-WFF; :: thesis: for f, f2 being FinSequence of PL-WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i holds
prc f2,F,i + n
let f, f2 be FinSequence of PL-WFF ; :: thesis: for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i holds
prc f2,F,i + n
let i, n be Nat; :: thesis: ( n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i implies prc f2,F,i + n )
assume that
A1: n + (len f) <= len f2 and
A2: for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) and
A3: 1 <= i and
A4: i <= len f ; :: thesis: ( not prc f,F,i or prc f2,F,i + n )
i + n <= (len f) + n by A4, XREAL_1:6;
then A5: i + n <= len f2 by A1, XXREAL_0:2;
A6: f /. i = f . i by A3, A4, LTLAXIO5:1
.= f2 . (i + n) by A2, A3, A4
.= f2 /. (i + n) by A3, A5, LTLAXIO5:1, NAT_1:12 ;
assume A7: prc f,F,i ; :: thesis: prc f2,F,i + n

per cases ( f . i in PL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) by A7;

suppose f . i in PL_axioms ; :: thesis: prc f2,F,i + n

hence prc f2,F,i + n by A2, A3, A4; :: thesis: verum

end;

suppose f . i in F ; :: thesis: prc f2,F,i + n

hence prc f2,F,i + n by A2, A3, A4; :: thesis: verum

end;

suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ; :: thesis: prc f2,F,i + n

then consider j, k being Nat such that
A8: 1 <= j and
A9: j < i and
A10: 1 <= k and
A11: k < i and
A12: f /. j,f /. k MP_rule f /. i ;
A13: ( 1 <= j + n & j + n < i + n ) by A8, A9, NAT_1:12, XREAL_1:8;
A14: k <= len f by A4, A11, XXREAL_0:2;
then k + n <= (len f) + n by XREAL_1:6;
then A15: k + n <= len f2 by A1, XXREAL_0:2;
A16: j <= len f by A4, A9, XXREAL_0:2;
then j + n <= (len f) + n by XREAL_1:6;
then A17: j + n <= len f2 by A1, XXREAL_0:2;
A18: f /. k = f . k by A10, A14, LTLAXIO5:1
.= f2 . (k + n) by A2, A10, A14
.= f2 /. (k + n) by A10, A15, LTLAXIO5:1, NAT_1:12 ;
A19: ( 1 <= k + n & k + n < i + n ) by A10, A11, NAT_1:12, XREAL_1:8;
f /. j = f . j by A8, A16, LTLAXIO5:1
.= f2 . (j + n) by A2, A8, A16
.= f2 /. (j + n) by A8, A17, LTLAXIO5:1, NAT_1:12 ;
hence prc f2,F,i + n by A6, A12, A13, A19, A18; :: thesis: verum

end;

end;