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 )

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 )

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

end;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

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
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;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

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

hence
f = carr g
by B1, PRALG_1:def 14, FINSEQ_3:29; :: thesis: verum
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;( 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