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
A7: 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
A8: 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 object st x in NAT holds
R1 . x = R2 . x
proof
let x be object ; :: thesis: ( x in NAT implies R1 . x = R2 . x )
assume x in NAT ; :: thesis: R1 . x = R2 . x
then reconsider x = x as Nat ;
now :: thesis: R1 . x = R2 . x
per cases ( L . x in W or not L . x in W ) ;
suppose A9: L . x in W ; :: thesis: R1 . x = R2 . x
then R1 . x = len (CastLTL (L . x)) by A7;
hence R1 . x = R2 . x by A8, A9; :: thesis: verum
end;
suppose A10: not L . x in W ; :: thesis: R1 . x = R2 . x
then R1 . x = 0 by A7;
hence R1 . x = R2 . x by A8, A10; :: thesis: verum
end;
end;
end;
hence R1 . x = R2 . x ; :: thesis: verum
end;
hence R1 = R2 by FUNCT_2:12; :: 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