let l be Nat; :: thesis: for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X & 1 <= l & l <= len f holds
(f . l) `1 in CnIPC X
let X be Subset of MC-wff; :: thesis: for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X & 1 <= l & l <= len f holds
(f . l) `1 in CnIPC X
let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( f is_a_proof_wrt_IPC X & 1 <= l & l <= len f implies (f . l) `1 in CnIPC X )
assume that
A1: f is_a_proof_wrt_IPC X and
A2: ( 1 <= l & l <= len f ) ; :: thesis: (f . l) `1 in CnIPC X
for n being Nat st 1 <= n & n <= len f holds
(f . n) `1 in CnIPC X

proof

defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies (f . $1) `1 in CnIPC X );
A3: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A4: for k being Nat st k < n holds
S₁[k] ; :: thesis: S₁[n]
assume that
A5: 1 <= n and
A6: n <= len f ; :: thesis: (f . n) `1 in CnIPC X
A7: f,n is_a_correct_step_wrt_IPC X by A1, A5, A6;

now :: thesis: (f . n) `1 in CnIPC X

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10 by A5, A6, Th3;

per cases then ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 or (f . n) `2 = 10 ) ;

suppose (f . n) `2 = 0 ; :: thesis: (f . n) `1 in CnIPC X

then A8: (f . n) `1 in X by A7, Def3;
X c= CnIPC X by INTPRO_1:12;
hence (f . n) `1 in CnIPC X by A8; :: thesis: verum

end;

suppose (f . n) `2 = 1 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q being Element of MC-wff st (f . n) `1 = p => (q => p) by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:1; :: thesis: verum

end;

suppose (f . n) `2 = 2 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q, r being Element of MC-wff st (f . n) `1 = (p => (q => r)) => ((p => q) => (p => r)) by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:2; :: thesis: verum

end;

suppose (f . n) `2 = 3 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => p by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:3; :: thesis: verum

end;

suppose (f . n) `2 = 4 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q being Element of MC-wff st (f . n) `1 = (p '&' q) => q by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:4; :: thesis: verum

end;

suppose (f . n) `2 = 5 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q being Element of MC-wff st (f . n) `1 = p => (q => (p '&' q)) by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:5; :: thesis: verum

end;

suppose (f . n) `2 = 6 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q being Element of MC-wff st (f . n) `1 = p => (p 'or' q) by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:6; :: thesis: verum

end;

suppose (f . n) `2 = 7 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q being Element of MC-wff st (f . n) `1 = q => (p 'or' q) by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:7; :: thesis: verum

end;

suppose (f . n) `2 = 8 ; :: thesis: (f . n) `1 in CnIPC X

then ex p, q, r being Element of MC-wff st (f . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:8; :: thesis: verum

end;

suppose (f . n) `2 = 9 ; :: thesis: (f . n) `1 in CnIPC X

then ex p being Element of MC-wff st (f . n) `1 = FALSUM => p by A7, Def3;
hence (f . n) `1 in CnIPC X by INTPRO_1:9; :: thesis: verum

end;

suppose (f . n) `2 = 10 ; :: thesis: (f . n) `1 in CnIPC X

then consider i, j being Nat, p, q being Element of MC-wff such that
A9: 1 <= i and
A10: i < n and
A11: 1 <= j and
A12: j < i and
A13: ( p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A7, Def3;
A14: j < n by A10, A12, XXREAL_0:2;
A15: i <= len f by A6, A10, XXREAL_0:2;
then j <= len f by A12, XXREAL_0:2;
then A16: (f . j) `1 in CnIPC X by A4, A11, A14;
(f . i) `1 in CnIPC X by A4, A9, A10, A15;
hence (f . n) `1 in CnIPC X by A13, A16, INTPRO_1:10; :: thesis: verum

end;

end;

end;

hence (f . n) `1 in CnIPC X ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A3);
hence for n being Nat st 1 <= n & n <= len f holds
(f . n) `1 in CnIPC X ; :: thesis: verum

end;

hence (f . l) `1 in CnIPC X by A2; :: thesis: verum