let c, d be set ; :: thesis: for f being FinSequence of CQC-WFF 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 ; :: 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 )
1 <= 2 ;
then A1: 1 <= len <*c,d*> by FINSEQ_1:61;
then 1 in dom <*c,d*> by FINSEQ_3:27;
then A2: (f ^ <*c,d*>) . ((len f) + 1) = <*c,d*> . 1 by FINSEQ_1:def 7;
A3: 2 <= len <*c,d*> by FINSEQ_1:61;
then 2 in dom <*c,d*> by FINSEQ_3:27;
then (f ^ <*c,d*>) . ((len f) + 2) = <*c,d*> . 2 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 A1, A2, A3, FINSEQ_1:61, FINSEQ_3:27; :: thesis: verum