let p, q be Element of MC-wff ; :: thesis: for X being Subset of MC-wff st p in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) } & p => q in { G where G is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = G ) } holds
q in { H where H is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = H ) }
let X be Subset of MC-wff; :: thesis: ( p in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) } & p => q in { G where G is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = G ) } implies q in { H where H is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = H ) } )
assume that
A1: p in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) } and
A2: p => q in { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) } ; :: thesis: q in { H where H is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = H ) }
ex t being Element of MC-wff st
( t = p & ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = t ) ) by A1;
then consider f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] such that
A3: f is_a_proof_wrt_IPC X and
A4: Effect_IPC f = p ;
ex r being Element of MC-wff st
( r = p => q & ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = r ) ) by A2;
then consider g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] such that
A5: g is_a_proof_wrt_IPC X and
A6: Effect_IPC g = p => q ;
reconsider qq = [q,10] as Element of [:MC-wff,Proof_Step_Kinds_IPC:] by Th1, ZFMISC_1:87;
set h = (f ^ g) ^ <*qq*>;
A7: len ((f ^ g) ^ <*qq*>) = (len (f ^ g)) + (len <*qq*>) by FINSEQ_1:22
.= (len (f ^ g)) + 1 by FINSEQ_1:40 ;
then A8: len ((f ^ g) ^ <*qq*>) = ((len f) + (len g)) + 1 by FINSEQ_1:22;
((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>)) = qq by A7, FINSEQ_1:42;
then (((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q ;
then A9: Effect_IPC ((f ^ g) ^ <*qq*>) = q by Def5;
for n being Nat st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X )
assume that
A10: 1 <= n and
A11: n <= len ((f ^ g) ^ <*qq*>) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X

now :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X

per cases ( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) ) by A8, A11, NAT_1:8;

suppose n <= (len f) + (len g) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X

then A12: n <= len (f ^ g) by FINSEQ_1:22;
f ^ g is_a_proof_wrt_IPC X by A3, A5, Th9;
then f ^ g,n is_a_correct_step_wrt_IPC X by A10, A12;
hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X by A10, A12, Th7; :: thesis: verum

end;

suppose A13: n = len ((f ^ g) ^ <*qq*>) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X

then ((f ^ g) ^ <*qq*>) . n = qq by A7, FINSEQ_1:42;
then A14: ( (((f ^ g) ^ <*qq*>) . n) `2 = 10 & (((f ^ g) ^ <*qq*>) . n) `1 = q ) ;
len f in Seg (len f) by A3, FINSEQ_1:3;
then A15: len f in dom f by FINSEQ_1:def 3;
(f ^ g) ^ <*qq*> = f ^ (g ^ <*qq*>) by FINSEQ_1:32;
then A16: (((f ^ g) ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by A15, FINSEQ_1:def 7
.= p by A4, A3, Def5 ;
( dom g = Seg (len g) & len g <> 0 ) by A5, FINSEQ_1:def 3;
then A17: len g in dom g by FINSEQ_1:3;
( 1 <= len f & len f <= (len f) + (len g) ) by A3, Th5, NAT_1:11;
then (len f) + (len g) in Seg ((len f) + (len g)) by FINSEQ_1:3;
then (len f) + (len g) in Seg (len (f ^ g)) by FINSEQ_1:22;
then (len f) + (len g) in dom (f ^ g) by FINSEQ_1:def 3;
then A18: (((f ^ g) ^ <*qq*>) . ((len f) + (len g))) `1 = ((f ^ g) . ((len f) + (len g))) `1 by FINSEQ_1:def 7
.= (g . (len g)) `1 by A17, FINSEQ_1:def 7
.= p => q by A6, A5, Def5 ;
1 <= len g by A5, Th5;
then (len f) + 1 <= (len f) + (len g) by XREAL_1:7;
then A19: len f < (len f) + (len g) by NAT_1:13;
A20: ( 1 <= len f & 1 <= (len f) + (len g) ) by A3, Th5, NAT_1:12;
(len f) + (len g) < n by A8, A13, NAT_1:13;
hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X by A14, A16, A18, A19, A20, Def3; :: thesis: verum

end;

end;

end;

hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt_IPC X ; :: thesis: verum

end;

then (f ^ g) ^ <*qq*> is_a_proof_wrt_IPC X ;
hence q in { H where H is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = H ) } by A9; :: thesis: verum