defpred S_{1}[ object , object ] means ( ( $1 = i implies $2 = (F . i) +* (j,v) ) & ( $1 <> i implies $2 = F . $1 ) );

A4: for x being object st x in I holds

ex y being object st S_{1}[x,y]

A7: ( dom f = I & ( for x being object st x in I holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A4);

reconsider f = f as ManySortedSet of I by A7, RELAT_1:def 18, PARTFUN1:def 2;

f is Function-yielding

f is ManySortedFunction of A,B

take f ; :: thesis: ( f . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

f . s = F . s ) )

thus f . i = (F . i) +* (j,v) by A1, A7; :: thesis: for s being set st s in I & s <> i holds

f . s = F . s

thus for s being set st s in I & s <> i holds

f . s = F . s by A7; :: thesis: verum

A4: for x being object st x in I holds

ex y being object st S

proof

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

assume x in I ; :: thesis: ex y being object st S_{1}[x,y]

end;assume x in I ; :: thesis: ex y being object st S

per cases
( x = i or x <> i )
;

end;

suppose A5:
x = i
; :: thesis: ex y being object st S_{1}[x,y]

take
(F . i) +* (j,v)
; :: thesis: S_{1}[x,(F . i) +* (j,v)]

thus S_{1}[x,(F . i) +* (j,v)]
by A5; :: thesis: verum

end;thus S

A7: ( dom f = I & ( for x being object st x in I holds

S

reconsider f = f as ManySortedSet of I by A7, RELAT_1:def 18, PARTFUN1:def 2;

f is Function-yielding

proof

then reconsider f = f as ManySortedFunction of I ;
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 f or f . x is set )

assume x in dom f ; :: thesis: f . x is set

then ( ( x = i implies f . x = (F . i) +* (j,v) ) & ( x <> i implies f . x = F . x ) ) by A7;

hence f . x is set ; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x is set

then ( ( x = i implies f . x = (F . i) +* (j,v) ) & ( x <> i implies f . x = F . x ) ) by A7;

hence f . x is set ; :: thesis: verum

f is ManySortedFunction of A,B

proof

then reconsider f = f as ManySortedFunction of A,B ;
reconsider j = j as Element of A . i by A2;

reconsider v = v as Element of B . i by A3;

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in I or f . x is Element of bool [:(A . x),(B . x):] )

assume x in I ; :: thesis: f . x is Element of bool [:(A . x),(B . x):]

then A8: ( S_{1}[x,f . x] & (F . i) +* (j,v) is Function of (A . i),(B . i) )
by A7;

thus f . x is Element of bool [:(A . x),(B . x):] by A8; :: thesis: verum

end;reconsider v = v as Element of B . i by A3;

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in I or f . x is Element of bool [:(A . x),(B . x):] )

assume x in I ; :: thesis: f . x is Element of bool [:(A . x),(B . x):]

then A8: ( S

thus f . x is Element of bool [:(A . x),(B . x):] by A8; :: thesis: verum

take f ; :: thesis: ( f . i = (F . i) +* (j,v) & ( for s being set st s in I & s <> i holds

f . s = F . s ) )

thus f . i = (F . i) +* (j,v) by A1, A7; :: thesis: for s being set st s in I & s <> i holds

f . s = F . s

thus for s being set st s in I & s <> i holds

f . s = F . s by A7; :: thesis: verum