let A be Element of LTLB_WFF ; :: thesis: for f being FinSequence of LTLB_WFF holds nega (f ^ <*A*>) = (nega f) ^ <*('not' A)*>
let f be FinSequence of LTLB_WFF ; :: thesis: nega (f ^ <*A*>) = (nega f) ^ <*('not' A)*>
set p = nega (f ^ <*A*>);
set q = (nega f) ^ <*('not' A)*>;
len (nega (f ^ <*A*>)) = len (f ^ <*A*>) by Def4;
then A1: dom (nega (f ^ <*A*>)) = dom (f ^ <*A*>) by FINSEQ_3:29;
A2: len (nega (f ^ <*A*>)) = len (f ^ <*A*>) by Def4
.= (len f) + (len <*A*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39
.= (len (nega f)) + 1 by Def4
.= (len (nega f)) + (len <*('not' A)*>) by FINSEQ_1:39
.= len ((nega f) ^ <*('not' A)*>) by FINSEQ_1:22 ;

now :: thesis: for j being Nat st j in dom (nega (f ^ <*A*>)) holds
(nega (f ^ <*A*>)) . j = ((nega f) ^ <*('not' A)*>) . j

let j be Nat; :: thesis: ( j in dom (nega (f ^ <*A*>)) implies (nega (f ^ <*A*>)) . b₁ = ((nega f) ^ <*('not' A)*>) . b₁ )
A3: len (f ^ <*A*>) = (len f) + (len <*A*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
assume A4: j in dom (nega (f ^ <*A*>)) ; :: thesis: (nega (f ^ <*A*>)) . b₁ = ((nega f) ^ <*('not' A)*>) . b₁
then A5: 1 <= j by FINSEQ_3:25;
j <= len (nega (f ^ <*A*>)) by A4, FINSEQ_3:25;
then A6: j <= (len f) + 1 by A3, Def4;
A7: j in dom ((nega f) ^ <*('not' A)*>) by A4, A2, FINSEQ_3:29;

per cases ( j = (len f) + 1 or j < (len f) + 1 ) by A6, XXREAL_0:1;

suppose A8: j = (len f) + 1 ; :: thesis: (nega (f ^ <*A*>)) . b₁ = ((nega f) ^ <*('not' A)*>) . b₁

then A9: j = (len (nega f)) + 1 by Def4;
thus (nega (f ^ <*A*>)) . j = (nega (f ^ <*A*>)) /. j by PARTFUN1:def 6, A4
.= 'not' ((f ^ <*A*>) /. j) by Th8, A4, A1
.= 'not' A by FINSEQ_4:67, A8
.= ((nega f) ^ <*('not' A)*>) /. j by A9, FINSEQ_4:67
.= ((nega f) ^ <*('not' A)*>) . j by PARTFUN1:def 6, A7 ; :: thesis: verum

end;

suppose j < (len f) + 1 ; :: thesis: (nega (f ^ <*A*>)) . b₁ = ((nega f) ^ <*('not' A)*>) . b₁

then A10: j <= len f by NAT_1:13;
then A11: j in dom f by A5, FINSEQ_3:25;
j <= len (nega f) by A10, Def4;
then A12: j in dom (nega f) by FINSEQ_3:25, A5;
thus (nega (f ^ <*A*>)) . j = (nega (f ^ <*A*>)) /. j by PARTFUN1:def 6, A4
.= 'not' ((f ^ <*A*>) /. j) by Th8, A4, A1
.= 'not' (f /. j) by FINSEQ_4:68, A11
.= (nega f) /. j by Th8, A11
.= ((nega f) ^ <*('not' A)*>) /. j by FINSEQ_4:68, A12
.= ((nega f) ^ <*('not' A)*>) . j by PARTFUN1:def 6, A7 ; :: thesis: verum

end;

end;

end;

hence nega (f ^ <*A*>) = (nega f) ^ <*('not' A)*> by FINSEQ_2:9, A2; :: thesis: verum