let X be set ; :: thesis: for S being Sequence st S = sequence_univers X holds
( last S = {} & S . NAT = {} )
let S be Sequence; :: thesis: ( S = sequence_univers X implies ( last S = {} & S . NAT = {} ) )
assume A1: S = sequence_univers X ; :: thesis: ( last S = {} & S . NAT = {} )
dom (sequence_univers X) = NAT by Def9;
hence ( last S = {} & S . NAT = {} ) by A1, Th91; :: thesis: verum