defpred S₁[ object , object ] means for j being Element of J st $1 = j holds
for o being operation of (A . j) st the charact of (A . j) . n = o holds
$2 = o;
A2: for x being object st x in J holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in J implies ex y being object st S₁[x,y] )
assume x in J ; :: thesis: ex y being object st S₁[x,y]
then reconsider x1 = x as Element of J ;
n in dom (signature (A . x1)) by A1, Def14;
then n in Seg (len (signature (A . x1))) by FINSEQ_1:def 3;
then n in Seg (len the charact of (A . x1)) by UNIALG_1:def 4;
then n in dom the charact of (A . x1) by FINSEQ_1:def 3;
then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def 3;
take o ; :: thesis: S₁[x,o]
let j be Element of J; :: thesis: ( x = j implies for o being operation of (A . j) st the charact of (A . j) . n = o holds
o = o )
assume A3: x = j ; :: thesis: for o being operation of (A . j) st the charact of (A . j) . n = o holds
o = o
let o1 be operation of (A . j); :: thesis: ( the charact of (A . j) . n = o1 implies o = o1 )
assume the charact of (A . j) . n = o1 ; :: thesis: o = o1
hence o = o1 by A3; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = J & ( for x being object st x in J holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
reconsider f = f as ManySortedSet of J by A4, PARTFUN1:def 2, RELAT_1:def 18;
for x being object st x in dom f holds
f . x is Function

proof

let x be object ; :: thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; :: thesis: f . x is Function
then reconsider x1 = x as Element of J by A4;
n in dom (signature (A . x1)) by A1, Def14;
then n in Seg (len (signature (A . x1))) by FINSEQ_1:def 3;
then n in Seg (len the charact of (A . x1)) by UNIALG_1:def 4;
then n in dom the charact of (A . x1) by FINSEQ_1:def 3;
then reconsider o = the charact of (A . x1) . n as operation of (A . x1) by FUNCT_1:def 3;
f . x = o by A4;
hence f . x is Function ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of J by FUNCOP_1:def 6;
for j being Element of J holds f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j)

proof

let j be Element of J; :: thesis: f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j)
AA: J = dom A by PARTFUN1:def 2;
n in dom (signature (A . j)) by A1, Def14;
then n in Seg (len (signature (A . j))) by FINSEQ_1:def 3;
then n in Seg (len the charact of (A . j)) by UNIALG_1:def 4;
then n in dom the charact of (A . j) by FINSEQ_1:def 3;
then reconsider o = the charact of (A . j) . n as operation of (A . j) by FUNCT_1:def 3;
( ex R being 1-sorted st
( R = A . j & (Carrier A) . j = the carrier of R ) & f . j = o ) by A4, Def13, AA;
hence f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j) ; :: thesis: verum

end;

then reconsider f = f as ManySortedOperation of Carrier A by Def15;
for i, j being Element of J holds arity (f . i) = arity (f . j)

proof

let i, j be Element of J; :: thesis: arity (f . i) = arity (f . j)
A5: n in dom (signature (A . j)) by A1, Def14;
then A6: n in Seg (len (signature (A . j))) by FINSEQ_1:def 3;
then n in Seg (len the charact of (A . j)) by UNIALG_1:def 4;
then n in dom the charact of (A . j) by FINSEQ_1:def 3;
then reconsider o = the charact of (A . j) . n as operation of (A . j) by FUNCT_1:def 3;
A7: (signature (A . j)) . n = arity o by A5, UNIALG_1:def 4;
dom A = J by PARTFUN1:def 2;
then A8: signature (A . i) = signature (A . j) by Def12;
then n in Seg (len the charact of (A . i)) by A6, UNIALG_1:def 4;
then n in dom the charact of (A . i) by FINSEQ_1:def 3;
then reconsider o1 = the charact of (A . i) . n as operation of (A . i) by FUNCT_1:def 3;
( arity (f . j) = arity o & f . i = o1 ) by A4;
hence arity (f . i) = arity (f . j) by A8, A5, A7, UNIALG_1:def 4; :: thesis: verum

end;

then reconsider f = f as equal-arity ManySortedOperation of Carrier A by Th11;
take f ; :: thesis: for j being Element of J
for o being operation of (A . j) st the charact of (A . j) . n = o holds
f . j = o
let j be Element of J; :: thesis: for o being operation of (A . j) st the charact of (A . j) . n = o holds
f . j = o
let o be operation of (A . j); :: thesis: ( the charact of (A . j) . n = o implies f . j = o )
assume the charact of (A . j) . n = o ; :: thesis: f . j = o
hence f . j = o by A4; :: thesis: verum