let I be set ; :: thesis: for A, B being ManySortedSet of
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 ; :: 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 18;
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 A2: ( f = F . i & g = (F || C) . i ) ; :: thesis: for x being set st x in C . i holds
g . x = f . x
then A3: g = Fi | (C . i) by A1, MSAFREE:def 1;
let x be set ; :: thesis: ( x in C . i implies g . x = f . x )
thus ( x in C . i implies g . x = f . x ) by A2, A3, FUNCT_1:72; :: thesis: verum