let X, Y be ManySortedFunction of C,B; :: thesis: ( ( for i being set st i in I holds

X . i = (F . i) | (C . i) ) & ( for i being set st i in I holds

Y . i = (F . i) | (C . i) ) implies X = Y )

assume that

A11: for i being set st i in I holds

X . i = (F . i) | (C . i) and

A12: for i being set st i in I holds

Y . i = (F . i) | (C . i) ; :: thesis: X = Y

let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or X . i = Y . i )

assume A13: i in I ; :: thesis: X . i = Y . i

then X . i = (F . i) | (C . i) by A11;

hence X . i = Y . i by A12, A13; :: thesis: verum

X . i = (F . i) | (C . i) ) & ( for i being set st i in I holds

Y . i = (F . i) | (C . i) ) implies X = Y )

assume that

A11: for i being set st i in I holds

X . i = (F . i) | (C . i) and

A12: for i being set st i in I holds

Y . i = (F . i) | (C . i) ; :: thesis: X = Y

let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or X . i = Y . i )

assume A13: i in I ; :: thesis: X . i = Y . i

then X . i = (F . i) | (C . i) by A11;

hence X . i = Y . i by A12, A13; :: thesis: verum