let f1, f2 be Function; :: thesis: ( dom f1 = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f1 . x = ERl PA ) ) & dom f2 = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f2 . x = ERl PA ) ) implies f1 = f2 )

assume that

A2: dom f1 = PARTITIONS Y and

A3: for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f1 . x = ERl PA ) and

A4: dom f2 = PARTITIONS Y and

A5: for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f2 . x = ERl PA ) ; :: thesis: f1 = f2

for z being object st z in PARTITIONS Y holds

f1 . z = f2 . z

ex PA being a_partition of Y st

( PA = x & f1 . x = ERl PA ) ) & dom f2 = PARTITIONS Y & ( for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f2 . x = ERl PA ) ) implies f1 = f2 )

assume that

A2: dom f1 = PARTITIONS Y and

A3: for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f1 . x = ERl PA ) and

A4: dom f2 = PARTITIONS Y and

A5: for x being object st x in PARTITIONS Y holds

ex PA being a_partition of Y st

( PA = x & f2 . x = ERl PA ) ; :: thesis: f1 = f2

for z being object st z in PARTITIONS Y holds

f1 . z = f2 . z

proof

hence
f1 = f2
by A2, A4, FUNCT_1:2; :: thesis: verum
let x be object ; :: thesis: ( x in PARTITIONS Y implies f1 . x = f2 . x )

assume x in PARTITIONS Y ; :: thesis: f1 . x = f2 . x

then ( ex PA being a_partition of Y st

( PA = x & f1 . x = ERl PA ) & ex PA being a_partition of Y st

( PA = x & f2 . x = ERl PA ) ) by A3, A5;

hence f1 . x = f2 . x ; :: thesis: verum

end;assume x in PARTITIONS Y ; :: thesis: f1 . x = f2 . x

then ( ex PA being a_partition of Y st

( PA = x & f1 . x = ERl PA ) & ex PA being a_partition of Y st

( PA = x & f2 . x = ERl PA ) ) by A3, A5;

hence f1 . x = f2 . x ; :: thesis: verum