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

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