defpred S_{1}[ 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_{1}[x,y]

A4: ( dom f = J & ( for x being object st x in J holds

S_{1}[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

for j being Element of J holds f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j)

for i, j being Element of J holds arity (f . i) = arity (f . j)

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

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

proof

consider f being Function such that
let x be object ; :: thesis: ( x in J implies ex y being object st S_{1}[x,y] )

assume x in J ; :: thesis: ex y being object st S_{1}[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_{1}[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;assume x in J ; :: thesis: ex y being object st S

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

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

A4: ( dom f = J & ( for x being object st x in J holds

S

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

then reconsider f = f as ManySortedFunction of J by FUNCOP_1:def 6;
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;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

for j being Element of J holds f . j is non empty homogeneous quasi_total PartFunc of (((Carrier A) . j) *),((Carrier A) . j)

proof

then reconsider f = f as ManySortedOperation of Carrier A by Def15;
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;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

for i, j being Element of J holds arity (f . i) = arity (f . j)

proof

then reconsider f = f as equal-arity ManySortedOperation of Carrier A by Th11;
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;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

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