let Al be QC-alphabet ; 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 ; 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; ( 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; verum