let X, Y be ManySortedFunction of C,B; :: thesis: ( ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
X . i = f | (C . i) ) & ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
Y . i = f | (C . i) ) implies X = Y )
assume that
A11: for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
X . i = f | (C . i) and
A12: for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
Y . i = f | (C . i) ; :: thesis: X = Y
for i being set st i in I holds
X . i = Y . i

proof

let i be set ; :: thesis: ( i in I implies X . i = Y . i )
assume A13: i in I ; :: thesis: X . i = Y . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 18;
X . i = f | (C . i) by A11, A13;
hence X . i = Y . i by A12, A13; :: thesis: verum

end;

hence X = Y by PBOOLE:3; :: thesis: verum