let X be set ; :: thesis: for Si being SigmaField of X
for f being Function holds
( f is SetSequence of Si iff f is sequence of Si )
let Si be SigmaField of X; :: thesis: for f being Function holds
( f is SetSequence of Si iff f is sequence of Si )
let f be Function; :: thesis: ( f is SetSequence of Si iff f is sequence of Si )
thus ( f is SetSequence of Si implies f is sequence of Si ) :: thesis: ( f is sequence of Si implies f is SetSequence of Si )

proof

assume f is SetSequence of Si ; :: thesis: f is sequence of Si
then reconsider f = f as SetSequence of Si ;
( rng f c= Si & dom f = NAT ) by Th1, FUNCT_2:def 1;
hence f is sequence of Si by FUNCT_2:2; :: thesis: verum

end;

assume A1: f is sequence of Si ; :: thesis: f is SetSequence of Si
then reconsider f = f as SetSequence of X by FUNCT_2:7;
f is SetSequence of Si by A1;
hence f is SetSequence of Si ; :: thesis: verum