let T1 be non empty 1-sorted ; :: thesis: for T2 being 1-sorted

for S being sequence of T1 st rng S c= the carrier of T2 holds

S is sequence of T2

let T2 be 1-sorted ; :: thesis: for S being sequence of T1 st rng S c= the carrier of T2 holds

S is sequence of T2

let S be sequence of T1; :: thesis: ( rng S c= the carrier of T2 implies S is sequence of T2 )

A1: dom S = NAT by FUNCT_2:def 1;

assume rng S c= the carrier of T2 ; :: thesis: S is sequence of T2

hence S is sequence of T2 by A1, FUNCT_2:2; :: thesis: verum

for S being sequence of T1 st rng S c= the carrier of T2 holds

S is sequence of T2

let T2 be 1-sorted ; :: thesis: for S being sequence of T1 st rng S c= the carrier of T2 holds

S is sequence of T2

let S be sequence of T1; :: thesis: ( rng S c= the carrier of T2 implies S is sequence of T2 )

A1: dom S = NAT by FUNCT_2:def 1;

assume rng S c= the carrier of T2 ; :: thesis: S is sequence of T2

hence S is sequence of T2 by A1, FUNCT_2:2; :: thesis: verum