let I be set ; :: thesis: for B being non-empty ManySortedSet of I
for C being ManySortedSet of I
for A being ManySortedSubset of C
for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
let B be non-empty ManySortedSet of I; :: thesis: for C being ManySortedSet of I
for A being ManySortedSubset of C
for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
let C be ManySortedSet of I; :: thesis: for A being ManySortedSubset of C
for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
let A be ManySortedSubset of C; :: thesis: for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F
let F be ManySortedFunction of A,B; :: thesis: ex G being ManySortedFunction of C,B st G || A = F
defpred S₁[ object , object , object ] means ex f being Function of (A . $3),(B . $3) st
( f = F . $3 & ( $2 in A . $3 implies $1 = f . $2 ) );
A1: for i being object st i in I holds
for x being object st x in C . i holds
ex y being object st
( y in B . i & S₁[y,x,i] )

proof

let i be object ; :: thesis: ( i in I implies for x being object st x in C . i holds
ex y being object st
( y in B . i & S₁[y,x,i] ) )
assume A2: i in I ; :: thesis: for x being object st x in C . i holds
ex y being object st
( y in B . i & S₁[y,x,i] )
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
let x be object ; :: thesis: ( x in C . i implies ex y being object st
( y in B . i & S₁[y,x,i] ) )
assume x in C . i ; :: thesis: ex y being object st
( y in B . i & S₁[y,x,i] )

per cases ( x in A . i or not x in A . i ) ;

suppose A3: x in A . i ; :: thesis: ex y being object st
( y in B . i & S₁[y,x,i] )

take f . x ; :: thesis: ( f . x in B . i & S₁[f . x,x,i] )
thus f . x in B . i by A2, A3, FUNCT_2:5; :: thesis: S₁[f . x,x,i]
take f ; :: thesis: ( f = F . i & ( x in A . i implies f . x = f . x ) )
thus ( f = F . i & ( x in A . i implies f . x = f . x ) ) ; :: thesis: verum

end;

suppose A4: not x in A . i ; :: thesis: ex y being object st
( y in B . i & S₁[y,x,i] )

consider y being object such that
A5: y in B . i by A2, XBOOLE_0:def 1;
take y ; :: thesis: ( y in B . i & S₁[y,x,i] )
thus y in B . i by A5; :: thesis: S₁[y,x,i]
take f ; :: thesis: ( f = F . i & ( x in A . i implies y = f . x ) )
thus ( f = F . i & ( x in A . i implies y = f . x ) ) by A4; :: thesis: verum

end;

end;

end;

consider G being ManySortedFunction of C,B such that
A6: for i being object st i in I holds
ex g being Function of (C . i),(B . i) st
( g = G . i & ( for x being object st x in C . i holds
S₁[g . x,x,i] ) ) from MSSUBFAM:sch 1(A1);
take G ; :: thesis: G || A = F

now :: thesis: for i being object st i in I holds
(G || A) . i = F . i

let i be object ; :: thesis: ( i in I implies (G || A) . i = F . i )
assume A7: i in I ; :: thesis: (G || A) . i = F . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
A8: dom f = A . i by A7, FUNCT_2:def 1;
consider g being Function of (C . i),(B . i) such that
A9: g = G . i and
A10: for x being object st x in C . i holds
S₁[g . x,x,i] by A6, A7;
A c= C by PBOOLE:def 18;
then A11: A . i c= C . i by A7;
A12: for x being object st x in A . i holds
f . x = (g | (A . i)) . x

proof

let x be object ; :: thesis: ( x in A . i implies f . x = (g | (A . i)) . x )
assume A13: x in A . i ; :: thesis: f . x = (g | (A . i)) . x
then ex h being Function of (A . i),(B . i) st
( h = F . i & ( x in A . i implies g . x = h . x ) ) by A10, A11;
hence f . x = (g | (A . i)) . x by A13, FUNCT_1:49; :: thesis: verum

end;

dom g = C . i by A7, FUNCT_2:def 1;
then A14: dom (g | (A . i)) = A . i by A11, RELAT_1:62;
thus (G || A) . i = g | (A . i) by A7, A9, MSAFREE:def 1
.= F . i by A8, A14, A12, FUNCT_1:2 ; :: thesis: verum

end;

hence G || A = F ; :: thesis: verum