let Al be QC-alphabet ; :: thesis: for c, d being object
for f being FinSequence of CQC-WFF Al holds
( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d )
let c, d be object ; :: thesis: for f being FinSequence of CQC-WFF Al holds
( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d )
let f be FinSequence of CQC-WFF Al; :: thesis: ( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d )
A1: 2 <= len <*c,d*> by FINSEQ_1:44;
then 2 in dom <*c,d*> by FINSEQ_3:25;
then A2: (f ^ <*c,d*>) . ((len f) + 2) = <*c,d*> . 2 by FINSEQ_1:def 7;
1 <= 2 ;
then A3: 1 <= len <*c,d*> by FINSEQ_1:44;
then 1 in dom <*c,d*> by FINSEQ_3:25;
then (f ^ <*c,d*>) . ((len f) + 1) = <*c,d*> . 1 by FINSEQ_1:def 7;
hence ( 1 in dom <*c,d*> & 2 in dom <*c,d*> & (f ^ <*c,d*>) . ((len f) + 1) = c & (f ^ <*c,d*>) . ((len f) + 2) = d ) by A3, A1, A2, FINSEQ_1:44, FINSEQ_3:25; :: thesis: verum