let n be Element of NAT ; :: thesis: for f being FinSequence of LTLB_WFF
for g being Function of LTLB_WFF,BOOLEAN st n in dom f holds
(VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n)))))
let f be FinSequence of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN st n in dom f holds
(VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n)))))
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: ( n in dom f implies (VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n))))) )
set v = VAL g;
assume n in dom f ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n)))))
then A1: ( 1 <= n & n <= len f ) by FINSEQ_3:25;
then f = ((f | (n -' 1)) ^ <*(f . n)*>) ^ (f /^ n) by FINSEQ_5:84
.= ((f | (n -' 1)) ^ <*(f /. n)*>) ^ (f /^ n) by FINSEQ_4:15, A1 ;
hence (VAL g) . H₂(f) = ((VAL g) . H₂((f | (n -' 1)) ^ <*(f /. n)*>)) '&' ((VAL g) . H₂(f /^ n)) by Th17
.= (((VAL g) . H₂(f | (n -' 1))) '&' ((VAL g) . H₂(<*(f /. n)*>))) '&' ((VAL g) . H₂(f /^ n)) by Th17
.= (((VAL g) . H₂(f | (n -' 1))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . H₂(f /^ n)) by Th11 ;
:: thesis: verum