set J = dom A;
defpred S₁[ 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₁[i,j]

proof

let i be object ; :: thesis: ( i in dom A implies ex j being object st S₁[i,j] )
assume A2: i in dom A ; :: thesis: ex j being object st S₁[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₁[i,j]

proof

reconsider R = A . i9 as 1-sorted by Def11a;
take j = the carrier of R; :: thesis: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

hence ex j being object st S₁[i,j] ; :: thesis: verum

end;

consider M being Function such that
A4: ( dom M = dom A & ( for i being object st i in dom A holds
S₁[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