let I be set ; :: thesis: for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let A, B be ManySortedSet of I; :: thesis: for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let C be ManySortedSubset of A; :: thesis: for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let F be ManySortedFunction of A,B; :: thesis: for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
let i be set ; :: thesis: ( i in I implies for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x )
assume A1: i in I ; :: thesis: for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x
then reconsider Fi = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
let f, g be Function; :: thesis: ( f = F . i & g = (F || C) . i implies for x being set st x in C . i holds
g . x = f . x )
assume that
A2: f = F . i and
A3: g = (F || C) . i ; :: thesis: for x being set st x in C . i holds
g . x = f . x
let x be set ; :: thesis: ( x in C . i implies g . x = f . x )
g = Fi | (C . i) by A1, A3, MSAFREE:def 1;
hence ( x in C . i implies g . x = f . x ) by A2, FUNCT_1:49; :: thesis: verum