let I be set ; 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; 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; 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; 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 ; ( 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
; 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; ( 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
; for x being set st x in C . i holds
g . x = f . x
let x be set ; ( 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; verum