let x be object ; :: thesis: ( x is real-valued Complex_Sequence iff x is Real_Sequence )
L1: for x being Real_Sequence holds x is real-valued Complex_Sequence

proof

let x be Real_Sequence; :: thesis: x is real-valued Complex_Sequence
( dom x = NAT & ( for k being Element of NAT holds x . k is Element of COMPLEX ) ) by SEQ_1:2, XCMPLX_0:def 2;
hence x is real-valued Complex_Sequence by COMSEQ_1:2; :: thesis: verum

end;

for x being real-valued Complex_Sequence holds x is Real_Sequence

proof

let x be real-valued Complex_Sequence; :: thesis: x is Real_Sequence
( dom x = NAT & ( for k being Nat holds x . k is real ) ) by COMSEQ_1:1;
hence x is Real_Sequence by SEQ_1:2; :: thesis: verum

end;

hence ( x is real-valued Complex_Sequence iff x is Real_Sequence ) by L1; :: thesis: verum