let g1, g2 be ManySortedFunction of dom f; :: thesis: ( ( for x being object st x in dom f holds

g1 . x = proj (f,x) ) & ( for x being object st x in dom f holds

g2 . x = proj (f,x) ) implies g1 = g2 )

assume that

A2: for x being object st x in dom f holds

g1 . x = proj (f,x) and

A3: for x being object st x in dom f holds

g2 . x = proj (f,x) ; :: thesis: g1 = g2

g1 . x = proj (f,x) ) & ( for x being object st x in dom f holds

g2 . x = proj (f,x) ) implies g1 = g2 )

assume that

A2: for x being object st x in dom f holds

g1 . x = proj (f,x) and

A3: for x being object st x in dom f holds

g2 . x = proj (f,x) ; :: thesis: g1 = g2

now :: thesis: for x being object st x in dom f holds

g1 . x = g2 . x

hence
g1 = g2
by PBOOLE:3; :: thesis: verumg1 . x = g2 . x

let x be object ; :: thesis: ( x in dom f implies g1 . x = g2 . x )

assume A4: x in dom f ; :: thesis: g1 . x = g2 . x

hence g1 . x = proj (f,x) by A2

.= g2 . x by A3, A4 ;

:: thesis: verum

end;assume A4: x in dom f ; :: thesis: g1 . x = g2 . x

hence g1 . x = proj (f,x) by A2

.= g2 . x by A3, A4 ;

:: thesis: verum