defpred S₁[ 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₁[x,y]

proof

let x be object ; :: thesis: ( x in I implies ex y being object st S₁[x,y] )
assume x in I ; :: thesis: ex y being object st S₁[x,y]

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

suppose A5: x = i ; :: thesis: ex y being object st S₁[x,y]

take (F . i) +* (j,v) ; :: thesis: S₁[x,(F . i) +* (j,v)]
thus S₁[x,(F . i) +* (j,v)] by A5; :: thesis: verum

end;

suppose A6: x <> i ; :: thesis: ex y being object st S₁[x,y]

take F . x ; :: thesis: S₁[x,F . x]
thus S₁[x,F . x] by A6; :: thesis: verum

end;

end;

end;

consider f being Function such that
A7: ( dom f = I & ( for x being object st x in I holds
S₁[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

proof

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;

then reconsider f = f as ManySortedFunction of I ;
f is ManySortedFunction of A,B

proof

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₁[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;

then reconsider f = f as 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