let f be Domain-Sequence; :: thesis:
thus ( f = carr g implies ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) ) ) :: thesis:

assume a0: f = carr g ; :: thesis:
then ( dom f = dom g & ( for j being set st j in dom g holds
ex R being 1-sorted st
( R = g . j & f . j = the carrier of R ) ) ) by PRALG_1:def 14;
for j being Element of dom g holds f . j = the carrier of (g . j)

let j be Element of dom g; :: thesis:
consider R being 1-sorted such that
A2: ( R = g . j & f . j = the carrier of R ) by a0, PRALG_1:def 14;
thus f . j = the carrier of (g . j) by A2; :: thesis:

end;

hence ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) ) by a0, FINSEQ_3:29, PRALG_1:def 14; :: thesis:

end;

assume B1: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) ) ; :: thesis:
for j being set st j in dom g holds
ex R being 1-sorted st
( R = g . j & f . j = the carrier of R )

let j be set ; :: thesis:
assume B3: j in dom g ; :: thesis:
then reconsider R = g . j as 1-sorted by PRALG_1:def 12;
take R ; :: thesis:
thus ( R = g . j & f . j = the carrier of R ) by B1, B3; :: thesis:

end;