let f be FinSequence of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN holds
( (VAL g) . ((con f) /. (len (con f))) = 1 iff for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 1 )
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: ( (VAL g) . ((con f) /. (len (con f))) = 1 iff for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 1 )
set v = VAL g;
defpred S₁[ Nat] means ( $1 <= len f implies (VAL g) . H₂(f | $1) = 1 );

hereby :: thesis: ( ( for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 1 ) implies (VAL g) . ((con f) /. (len (con f))) = 1 )

assume A1: (VAL g) . H₂(f) = 1 ; :: thesis: for i being Nat holds
( not i in dom f or (VAL g) . (f /. i) = 1 )
given i being Nat such that A2: i in dom f and
A3: not (VAL g) . (f /. i) = 1 ; :: thesis: contradiction
A4: i <= len f by A2, FINSEQ_3:25;
( f /. i = f . i & 1 <= i ) by PARTFUN1:def 6, A2, FINSEQ_3:25;
then f = ((f | (i -' 1)) ^ <*(f /. i)*>) ^ (f /^ i) by A4, FINSEQ_5:84;
then A5: (VAL g) . H₂(f) = ((VAL g) . H₂((f | (i -' 1)) ^ <*(f /. i)*>)) '&' ((VAL g) . H₂(f /^ i)) by Th17
.= (((VAL g) . H₂(f | (i -' 1))) '&' ((VAL g) . H₂(<*(f /. i)*>))) '&' ((VAL g) . H₂(f /^ i)) by Th17
.= (((VAL g) . H₂(f | (i -' 1))) '&' ((VAL g) . H₂(f /^ i))) '&' ((VAL g) . H₂(<*(f /. i)*>)) ;
(VAL g) . H₂(<*(f /. i)*>) = (VAL g) . (f /. i) by Th11
.= 0 by A3, XBOOLEAN:def 3 ;
hence contradiction by A5, A1; :: thesis: verum

end;

assume A6: for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 1 ; :: thesis: (VAL g) . ((con f) /. (len (con f))) = 1

A7: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

A9: 1 <= k + 1 by NAT_1:11;
assume A10: k + 1 <= len f ; :: thesis: (VAL g) . H₂(f | (k + 1)) = 1
then f | (k + 1) = (f | k) ^ <*(f . (k + 1))*> by NAT_1:13, FINSEQ_5:83
.= (f | k) ^ <*(f /. (k + 1))*> by FINSEQ_4:15, NAT_1:11, A10 ;
hence (VAL g) . H₂(f | (k + 1)) = ((VAL g) . H₂(f | k)) '&' ((VAL g) . H₂(<*(f /. (k + 1))*>)) by Th17
.= ((VAL g) . H₂(f | k)) '&' ((VAL g) . (f /. (k + 1))) by Th11
.= 1 by A6, A9, FINSEQ_3:25, A10, A8, NAT_1:13 ;
:: thesis: verum

end;

end;

A11: S₁[ 0 ] by Th10, Th4;
A12: for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A7);
f = f | (len f) by FINSEQ_1:58;
hence (VAL g) . H₂(f) = 1 by A12; :: thesis: verum