let l be Element of NAT ; :: thesis: for X being Subset of CQC-WFF
for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X & 1 <= l & l <= len f holds
(f . l) `1 in Cn X
let X be Subset of CQC-WFF ; :: thesis: for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X & 1 <= l & l <= len f holds
(f . l) `1 in Cn X
let f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; :: thesis: ( f is_a_proof_wrt X & 1 <= l & l <= len f implies (f . l) `1 in Cn X )
assume that
A1: f is_a_proof_wrt X and
A2: ( 1 <= l & l <= len f ) ; :: thesis: (f . l) `1 in Cn X
for n being Element of NAT st 1 <= n & n <= len f holds
(f . n) `1 in Cn X

proof

defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies (f . $1) `1 in Cn 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]
A5: n in NAT by ORDINAL1:def 13;
assume A6: ( 1 <= n & n <= len f ) ; :: thesis: (f . n) `1 in Cn X
then A7: f,n is_a_correct_step_wrt X by A1, A5, Def5;

now

per cases ( (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 ) by A6, Th45;

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

then ( (f . n) `1 in X & X c= Cn X ) by A7, Def4, Th38;
hence (f . n) `1 in Cn X ; :: thesis: verum

end;

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

then (f . n) `1 = VERUM by A7, Def4;
hence (f . n) `1 in Cn X by Th27; :: thesis: verum

end;

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

then ex p being Element of CQC-WFF st (f . n) `1 = (('not' p) => p) => p by A7, Def4;
hence (f . n) `1 in Cn X by Th28; :: thesis: verum

end;

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

then ex p, q being Element of CQC-WFF st (f . n) `1 = p => (('not' p) => q) by A7, Def4;
hence (f . n) `1 in Cn X by Th29; :: thesis: verum

end;

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

then ex p, q, r being Element of CQC-WFF st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A7, Def4;
hence (f . n) `1 in Cn X by Th30; :: thesis: verum

end;

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

then ex p, q being Element of CQC-WFF st (f . n) `1 = (p '&' q) => (q '&' p) by A7, Def4;
hence (f . n) `1 in Cn X by Th31; :: thesis: verum

end;

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

then ex p being Element of CQC-WFF ex x being bound_QC-variable st (f . n) `1 = (All x,p) => p by A7, Def4;
hence (f . n) `1 in Cn X by Th33; :: thesis: verum

end;

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

then consider i, j being Element of NAT , p, q being Element of CQC-WFF such that
A8: ( 1 <= i & i < n & 1 <= j & j < i ) and
A9: p = (f . j) `1 and
A10: q = (f . n) `1 and
A11: (f . i) `1 = p => q by A7, Def4;
A12: j < n by A8, XXREAL_0:2;
( 1 <= i & i <= len f ) by A6, A8, XXREAL_0:2;
then ( 1 <= i & i <= len f & 1 <= j & j <= len f ) by A8, XXREAL_0:2;
then ( (f . j) `1 in Cn X & (f . i) `1 in Cn X ) by A4, A8, A12;
hence (f . n) `1 in Cn X by A9, A10, A11, Th32; :: thesis: verum

end;

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

then consider i being Element of NAT , p, q being Element of CQC-WFF , x being bound_QC-variable such that
A13: ( 1 <= i & i < n ) and
A14: (f . i) `1 = p => q and
A15: not x in still_not-bound_in p and
A16: (f . n) `1 = p => (All x,q) by A7, Def4;
( 1 <= i & i <= len f ) by A6, A13, XXREAL_0:2;
hence (f . n) `1 in Cn X by A4, A13, A14, A15, A16, Th34; :: thesis: verum

end;

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

then consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A17: ( 1 <= i & i < n ) and
A18: ( s . x in CQC-WFF & s . y in CQC-WFF ) and
A19: not x in still_not-bound_in s and
A20: s . x = (f . i) `1 and
A21: (f . n) `1 = s . y by A7, Def4;
( 1 <= i & i <= len f ) by A6, A17, XXREAL_0:2;
hence (f . n) `1 in Cn X by A4, A17, A18, A19, A20, A21, Th35; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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