set J = dom A;

defpred S_{1}[ object , object ] means ex R being 1-sorted st

( R = A . $1 & $2 = the carrier of R );

A1: for i being object st i in dom A holds

ex j being object st S_{1}[i,j]

A4: ( dom M = dom A & ( for i being object st i in dom A holds

S_{1}[i,M . i] ) )
from CLASSES1:sch 1(A1);

take M ; :: thesis: ( dom M = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & M . j = the carrier of R ) ) )

thus ( dom M = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & M . j = the carrier of R ) ) ) by A4; :: thesis: verum

defpred S

( R = A . $1 & $2 = the carrier of R );

A1: for i being object st i in dom A holds

ex j being object st S

proof

consider M being Function such that
let i be object ; :: thesis: ( i in dom A implies ex j being object st S_{1}[i,j] )

assume A2: i in dom A ; :: thesis: ex j being object st S_{1}[i,j]

then reconsider J = dom A as non empty set ;

reconsider i9 = i as Element of J by A2;

ex j being object st S_{1}[i,j]
_{1}[i,j]
; :: thesis: verum

end;assume A2: i in dom A ; :: thesis: ex j being object st S

then reconsider J = dom A as non empty set ;

reconsider i9 = i as Element of J by A2;

ex j being object st S

proof

hence
ex j being object st S
reconsider R = A . i9 as 1-sorted by Def11a;

take j = the carrier of R; :: thesis: S_{1}[i,j]

thus S_{1}[i,j]
; :: thesis: verum

end;take j = the carrier of R; :: thesis: S

thus S

A4: ( dom M = dom A & ( for i being object st i in dom A holds

S

take M ; :: thesis: ( dom M = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & M . j = the carrier of R ) ) )

thus ( dom M = dom A & ( for j being set st j in dom A holds

ex R being 1-sorted st

( R = A . j & M . j = the carrier of R ) ) ) by A4; :: thesis: verum