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 reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 18;
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] )

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

suppose A3: 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 A2, A3, 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 A4: 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
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 ) & ( 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 A4; :: 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
A6: 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 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 18;
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 set st x in C . i holds
S₁[g . x,x,i] by A6, A7;
A c= C by PBOOLE:def 23;
then A11: A . i c= C . i by A7, PBOOLE:def 5;
A12: 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 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 ) & ( not x in A . i implies verum ) ) by A10, A11;
hence f . x = (g | (A . i)) . x by A13, FUNCT_1:72; :: 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:91;
thus (G || A) . i = g | (A . i) by A7, A9, MSAFREE:def 1
.= F . i by A8, A14, A12, FUNCT_1:9 ; :: thesis: verum

end;

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