let I be set ; :: thesis: for I0 being Subset of I
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds
F | I0 is ManySortedFunction of A0,B0
let I0 be Subset of I; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds
F | I0 is ManySortedFunction of A0,B0
let A, B be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds
F | I0 is ManySortedFunction of A0,B0
let F be ManySortedFunction of A,B; :: thesis: for A0, B0 being ManySortedSet of I0 st A0 = A | I0 & B0 = B | I0 holds
F | I0 is ManySortedFunction of A0,B0
let A0, B0 be ManySortedSet of I0; :: thesis: ( A0 = A | I0 & B0 = B | I0 implies F | I0 is ManySortedFunction of A0,B0 )
assume A1: ( A0 = A | I0 & B0 = B | I0 ) ; :: thesis: F | I0 is ManySortedFunction of A0,B0
A2: dom A0 = I0 by PBOOLE:def 3;
A3: dom B0 = I0 by PBOOLE:def 3;
A4: dom (F | I0) = I0 by PBOOLE:def 3;
reconsider G = F | I0 as ManySortedFunction of I0 ;

now

let i be set ; :: thesis: ( i in I0 implies G . i is Function of A0 . i,B0 . i )
assume A5: i in I0 ; :: thesis: G . i is Function of A0 . i,B0 . i
then A6: G . i = F . i by A4, FUNCT_1:70;
( A . i = A0 . i & B . i = B0 . i ) by A1, A2, A3, A5, FUNCT_1:70;
hence G . i is Function of A0 . i,B0 . i by A5, A6, PBOOLE:def 18; :: thesis: verum

end;

hence F | I0 is ManySortedFunction of A0,B0 by PBOOLE:def 18; :: thesis: verum