let R1, R2 be Real_Sequence; ( ( for k being Nat holds
( ( L . k in W implies R1 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies R1 . k = 0 ) ) ) & ( for k being Nat holds
( ( L . k in W implies R2 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies R2 . k = 0 ) ) ) implies R1 = R2 )
( ( for k being Nat holds
( ( L . k in W implies R1 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies R1 . k = 0 ) ) ) & ( for k being Nat holds
( ( L . k in W implies R2 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies R2 . k = 0 ) ) ) implies R1 = R2 )
hence
( ( for k being Nat holds
( ( L . k in W implies R1 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies R1 . k = 0 ) ) ) & ( for k being Nat holds
( ( L . k in W implies R2 . k = len (CastLTL (L . k)) ) & ( not L . k in W implies R2 . k = 0 ) ) ) implies R1 = R2 )
; verum