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

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

hence
g1 = g2
; :: thesis: verumg1 . 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;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