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