deffunc H₁( set ) -> Nat = Length_fun (L,W,$1);
A1: for x being set st x in NAT holds
H₁(x) in REAL by ORDINAL1:def 12, NUMBERS:19;
consider IT being sequence of REAL such that
A2: for x being set st x in NAT holds
IT . x = H₁(x) from FUNCT_2:sch 11(A1);
take IT ; :: thesis: for k being Nat holds
( ( L . k in W implies IT . k = len (CastLTL (L . k)) ) & ( not L . k in W implies IT . k = 0 ) )
for k being Nat holds
( ( L . k in W implies IT . k = len (CastLTL (L . k)) ) & ( not L . k in W implies IT . k = 0 ) )

proof

let k be Nat; :: thesis: ( ( L . k in W implies IT . k = len (CastLTL (L . k)) ) & ( not L . k in W implies IT . k = 0 ) )
A3: k in NAT by ORDINAL1:def 12;
A4: ( not L . k in W implies IT . k = 0 )

proof

assume A5: not L . k in W ; :: thesis: IT . k = 0
IT . k = Length_fun (L,W,k) by A2, A3;
hence IT . k = 0 by A5, Def23; :: thesis: verum

end;

( L . k in W implies IT . k = len (CastLTL (L . k)) )

proof

assume A6: L . k in W ; :: thesis: IT . k = len (CastLTL (L . k))
IT . k = Length_fun (L,W,k) by A2, A3;
hence IT . k = len (CastLTL (L . k)) by A6, Def23; :: thesis: verum

end;

hence ( ( L . k in W implies IT . k = len (CastLTL (L . k)) ) & ( not L . k in W implies IT . k = 0 ) ) by A4; :: thesis: verum

end;

hence for k being Nat holds
( ( L . k in W implies IT . k = len (CastLTL (L . k)) ) & ( not L . k in W implies IT . k = 0 ) ) ; :: thesis: verum