deffunc H₁( set ) -> Nat = Length_fun L,W,$1;
A1: for x being set st x in NAT holds
H₁(x) in REAL

proof

let x be set ; :: thesis: ( x in NAT implies H₁(x) in REAL )
assume x in NAT ; :: thesis: H₁(x) in REAL
H₁(x) in NAT by ORDINAL1:def 13;
hence H₁(x) in REAL ; :: thesis: verum

end;

consider IT being Function of NAT ,REAL such that
A2: for x being set st x in NAT holds
IT . x = H₁(x) from FUNCT_2:sch 2(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 13;
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