let g1, g2 be ManySortedFunction of I; :: thesis: ( ( for i being object st i in I holds
g1 . i = f | (A . i) ) & ( for i being object st i in I holds
g2 . i = f | (A . i) ) implies g1 = g2 )
assume that
A2: for i being object st i in I holds
g1 . i = f | (A . i) and
A3: for i being object st i in I holds
g2 . i = f | (A . i) ; :: thesis: g1 = g2

now :: thesis: for i being object st i in I holds
g1 . i = g2 . i

let i be object ; :: thesis: ( i in I implies g1 . i = g2 . i )
assume A4: i in I ; :: thesis: g1 . i = g2 . i
then g1 . i = f | (A . i) by A2;
hence g1 . i = g2 . i by A3, A4; :: thesis: verum

end;

hence g1 = g2 ; :: thesis: verum