let p be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF
for f, f1 being FinSequence of PL-WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ) & prc f,F, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & F |- p )
let F be Subset of PL-WFF; :: thesis: for f, f1 being FinSequence of PL-WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ) & prc f,F, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & F |- p )
let f, f1 be FinSequence of PL-WFF ; :: thesis: ( f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ) & prc f,F, len f implies ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & F |- p ) )
assume that
A1: f = f1 ^ <*p*> and
1 <= len f1 and
A2: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ; :: thesis: ( not prc f,F, len f or ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & F |- p ) )
A3: len f = (len f1) + (len <*p*>) by A1, FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
assume A4: prc f,F, len f ; :: thesis: ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & F |- p )
A5: 0 + (len f1) <= len f by A3, NAT_1:12;

A6: now :: thesis: for i being Nat st 1 <= i & i <= len f holds
prc f,F,i

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc f,F,b₁ )
assume that
A7: 1 <= i and
A8: i <= len f ; :: thesis: prc f,F,b₁
A9: ( i < (len f1) + 1 or i = (len f1) + 1 ) by A3, A8, XXREAL_0:1;
A10: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f . (k + 0) by A1, FINSEQ_1:64;

per cases ( i <= len f1 or i = len f ) by A3, A9, NAT_1:13;

suppose i <= len f1 ; :: thesis: prc f,F,b₁

then prc f,F,i + 0 by A2, A5, A7, A10, Th38;
hence prc f,F,i ; :: thesis: verum

end;

suppose i = len f ; :: thesis: prc f,F,b₁

hence prc f,F,i by A4; :: thesis: verum

end;

end;

end;

hence for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ; :: thesis: F |- p
f . (len f) = f . ((len f1) + (len <*p*>)) by A1, FINSEQ_1:22
.= f . ((len f1) + 1) by FINSEQ_1:39
.= p by A1, FINSEQ_1:42 ;
hence F |- p by A3, XREAL_1:31, A6; :: thesis: verum