let f, f1 be FinSequence of LTLB_WFF ; :: thesis: nega (f ^ f1) = (nega f) ^ (nega f1)
set c1 = nega (f ^ f1);
set c2 = (nega f) ^ (nega f1);
A1: len (nega (f ^ f1)) = len (f ^ f1) by Def4
.= (len f) + (len f1) by FINSEQ_1:22
.= (len f) + (len (nega f1)) by Def4
.= (len (nega f)) + (len (nega f1)) by Def4
.= len ((nega f) ^ (nega f1)) by FINSEQ_1:22 ;

now :: thesis: for j being Nat st j in dom (nega (f ^ f1)) holds
(nega (f ^ f1)) . j = ((nega f) ^ (nega f1)) . j

let j be Nat; :: thesis: ( j in dom (nega (f ^ f1)) implies (nega (f ^ f1)) . b₁ = ((nega f) ^ (nega f1)) . b₁ )
assume A2: j in dom (nega (f ^ f1)) ; :: thesis: (nega (f ^ f1)) . b₁ = ((nega f) ^ (nega f1)) . b₁
then A3: 1 <= j by FINSEQ_3:25;
j <= len (nega (f ^ f1)) by A2, FINSEQ_3:25;
then A4: j <= len (f ^ f1) by Def4;
then A5: j in dom (f ^ f1) by FINSEQ_3:25, A3;
A6: j in dom ((nega f) ^ (nega f1)) by A2, A1, FINSEQ_3:29;

per cases ( j <= len f or j > len f ) ;

suppose A7: j <= len f ; :: thesis: (nega (f ^ f1)) . b₁ = ((nega f) ^ (nega f1)) . b₁

then j <= len (nega f) by Def4;
then A8: j in dom (nega f) by A3, FINSEQ_3:25;
A9: j in dom f by A7, A3, FINSEQ_3:25;
thus (nega (f ^ f1)) . j = (nega (f ^ f1)) /. j by PARTFUN1:def 6, A2
.= 'not' ((f ^ f1) /. j) by Th8, A5
.= 'not' (f /. j) by FINSEQ_4:68, A9
.= (nega f) /. j by Th8, A9
.= ((nega f) ^ (nega f1)) /. j by FINSEQ_4:68, A8
.= ((nega f) ^ (nega f1)) . j by PARTFUN1:def 6, A6 ; :: thesis: verum

end;

suppose A10: j > len f ; :: thesis: (nega (f ^ f1)) . b₁ = ((nega f) ^ (nega f1)) . b₁

then consider k being Nat such that
A11: j = (len f) + k by NAT_1:10;

A12: now :: thesis: not k > len f1

assume k > len f1 ; :: thesis: contradiction
then j > (len f1) + (len f) by XREAL_1:8, A11;
hence contradiction by A4, FINSEQ_1:22; :: thesis: verum

end;

( k = 0 or k > 0 ) ;
then A13: 1 <= k by NAT_1:25, A11, A10;
then A14: k in dom f1 by A12, FINSEQ_3:25;
A15: j = (len (nega f)) + k by A11, Def4;
k <= len (nega f1) by Def4, A12;
then A16: k in dom (nega f1) by A13, FINSEQ_3:25;
thus (nega (f ^ f1)) . j = (nega (f ^ f1)) /. j by PARTFUN1:def 6, A2
.= 'not' ((f ^ f1) /. j) by Th8, A5
.= 'not' (f1 /. k) by FINSEQ_4:69, A14, A11
.= (nega f1) /. k by Th8, A14
.= ((nega f) ^ (nega f1)) /. j by FINSEQ_4:69, A16, A15
.= ((nega f) ^ (nega f1)) . j by PARTFUN1:def 6, A6 ; :: thesis: verum

end;

end;

end;

hence nega (f ^ f1) = (nega f) ^ (nega f1) by FINSEQ_2:9, A1; :: thesis: verum