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 that
A1: A0 = A | I0 and
A2: B0 = B | I0 ; :: thesis: F | I0 is ManySortedFunction of A0,B0
reconsider G = F | I0 as ManySortedFunction of I0 ;
A3: ( dom A0 = I0 & dom (F | I0) = I0 ) by PARTFUN1:def 2;
A4: dom B0 = I0 by PARTFUN1:def 2;
now :: thesis: for i being object st i in I0 holds
G . i is Function of (A0 . i),(B0 . i)
let i be object ; :: 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: B . i = B0 . i by A2, A4, FUNCT_1:47;
( G . i = F . i & A . i = A0 . i ) by A1, A3, A5, FUNCT_1:47;
hence G . i is Function of (A0 . i),(B0 . i) by A5, A6, PBOOLE:def 15; :: thesis: verum
end;
hence F | I0 is ManySortedFunction of A0,B0 by PBOOLE:def 15; :: thesis: verum