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