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) ) )
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)
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 ;
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 ; :: 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 ; :: thesis: verum