let I be set ; :: thesis: for B being V2() ManySortedSet of
for C being ManySortedSet of
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 V2() ManySortedSet of ; :: thesis: for C being ManySortedSet of
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 ; :: 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₁[ set , set , set ] means ex f being Function of (A . $3),(B . $3) st
( f = F . $3 & ( $2 in A . $3 implies $1 = f . $2 ) & ( not $2 in A . $3 implies verum ) );
A1: for i being set st i in I holds
for x being set st x in C . i holds
ex y being set st
( y in B . i & S₁[y,x,i] )

proof

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

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

suppose A4: x in A . i ; :: thesis: ex y being set 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 A3, A4, FUNCT_2:7; :: thesis: S₁[f . x,x,i]
take f ; :: thesis: ( f = F . i & ( x in A . i implies f . x = f . x ) & ( not x in A . i implies verum ) )
thus ( f = F . i & ( x in A . i implies f . x = f . x ) & ( not x in A . i implies verum ) ) ; :: thesis: verum

end;

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

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

end;

end;

end;

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

now

let i be set ; :: thesis: ( i in I implies (G || A) . i = F . i )
assume A8: i in I ; :: thesis: (G || A) . i = F . i
then A9: B . i <> {} ;
reconsider f = F . i as Function of (A . i),(B . i) by A8, PBOOLE:def 18;
consider g being Function of (C . i),(B . i) such that
A10: g = G . i and
A11: for x being set st x in C . i holds
S₁[g . x,x,i] by A7, A8;
A12: dom f = A . i by A9, FUNCT_2:def 1;
A c= C by PBOOLE:def 23;
then A13: A . i c= C . i by A8, PBOOLE:def 5;
dom g = C . i by A9, FUNCT_2:def 1;
then A14: dom (g | (A . i)) = A . i by A13, RELAT_1:91;
A15: for x being set st x in A . i holds
f . x = (g | (A . i)) . x

proof

let x be set ; :: thesis: ( x in A . i implies f . x = (g | (A . i)) . x )
assume A16: x in A . i ; :: thesis: f . x = (g | (A . i)) . x
then consider h being Function of (A . i),(B . i) such that
A17: ( h = F . i & ( x in A . i implies g . x = h . x ) ) and
( not x in A . i implies verum ) by A11, A13;
thus f . x = (g | (A . i)) . x by A16, A17, FUNCT_1:72; :: thesis: verum

end;

thus (G || A) . i = g | (A . i) by A8, A10, MSAFREE:def 1
.= F . i by A12, A14, A15, FUNCT_1:9 ; :: thesis: verum

end;

hence G || A = F by PBOOLE:3; :: thesis: verum