let R1, R2 be Real_Sequence; :: thesis: ( ( 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 )

proof

assume that
B1: 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 ) ) and
B2: 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 ) ) ; :: thesis: R1 = R2
for x being set st x in NAT holds
R1 . x = R2 . x

proof

let x be set ; :: thesis: ( x in NAT implies R1 . x = R2 . x )
assume A1: x in NAT ; :: thesis: R1 . x = R2 . x
reconsider x = x as Nat by A1;

now

per cases ( L . x in W or not L . x in W ) ;

suppose C1: L . x in W ; :: thesis: R1 . x = R2 . x

then R1 . x = len (CastLTL (L . x)) by B1;
hence R1 . x = R2 . x by C1, B2; :: thesis: verum

end;

suppose C2: not L . x in W ; :: thesis: R1 . x = R2 . x

then R1 . x = 0 by B1;
hence R1 . x = R2 . x by C2, B2; :: thesis: verum

end;

end;

end;

hence R1 . x = R2 . x ; :: thesis: verum

end;

hence R1 = R2 by FUNCT_2:18; :: thesis: verum

end;

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 ) ; :: thesis: verum