let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
& p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}
holds
q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = H )
}

let p, q be Element of CQC-WFF Al; :: thesis: for X being Subset of (CQC-WFF Al) st p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
& p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}
holds
q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = H )
}

let X be Subset of (CQC-WFF Al); :: thesis: ( p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
& p => q in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}
implies q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = H )
}
)

assume that
A1: p in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
and
A2: p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
; :: thesis: q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = H )
}

ex t being Element of CQC-WFF Al st
( t = p & ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = t ) ) by A1;
then consider f being FinSequence of such that
A3: f is_a_proof_wrt X and
A4: Effect f = p ;
ex r being Element of CQC-WFF Al st
( r = p => q & ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = r ) ) by A2;
then consider g being FinSequence of such that
A5: g is_a_proof_wrt X and
A6: Effect g = p => q ;
reconsider qq = [q,7] as Element of by ;
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 ;
then (((f ^ g) ^ <*qq*>) . (len ((f ^ g) ^ <*qq*>))) `1 = q ;
then A9: Effect ((f ^ g) ^ <*qq*>) = q by Def6;
for n being Nat st 1 <= n & n <= len ((f ^ g) ^ <*qq*>) holds
(f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len ((f ^ g) ^ <*qq*>) implies (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X )
assume that
A10: 1 <= n and
A11: n <= len ((f ^ g) ^ <*qq*>) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
now :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
per cases ( n <= (len f) + (len g) or n = len ((f ^ g) ^ <*qq*>) ) by ;
suppose A13: n = len ((f ^ g) ^ <*qq*>) ; :: thesis: (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X
then ((f ^ g) ^ <*qq*>) . n = qq by ;
then A14: ( (((f ^ g) ^ <*qq*>) . n) `2 = 7 & (((f ^ g) ^ <*qq*>) . n) `1 = q ) ;
len f <> 0 by A3;
then len f in Seg (len f) by 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
.= p by A4, A3, Def6 ;
( dom g = Seg (len g) & len g <> 0 ) by ;
then A17: len g in dom g by FINSEQ_1:3;
( 1 <= len f & len f <= (len f) + (len g) ) by ;
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
.= p => q by A6, A5, Def6 ;
1 <= len g by ;
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 ;
(len f) + (len g) < n by ;
hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X by A14, A16, A18, A19, A20, Def4; :: thesis: verum
end;
end;
end;
hence (f ^ g) ^ <*qq*>,n is_a_correct_step_wrt X ; :: thesis: verum
end;
then (f ^ g) ^ <*qq*> is_a_proof_wrt X ;
hence q in { H where H is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = H )
}
by A9; :: thesis: verum