let f be Domain-Sequence; :: thesis: ( f = carr g iff ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) ) )
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: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) implies f = carr g )

proof

assume a0: f = carr g ; :: thesis: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) )
for j being Element of dom g holds f . j = the carrier of (g . j)

proof

let j be Element of dom g; :: thesis: f . j = the carrier of (g . j)
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: verum

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: verum

end;

assume B1: ( len f = len g & ( for j being Element of dom g holds f . j = the carrier of (g . j) ) ) ; :: thesis: f = carr 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 )

proof

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

end;

hence f = carr g by B1, PRALG_1:def 14, FINSEQ_3:29; :: thesis: verum