let f1, f2 be map of R; :: thesis: ( ( for x being Subset of R holds f1 . x = { u where u is Element of R : f . u meets x } ) & ( for x being Subset of R holds f2 . x = { u where u is Element of R : f . u meets x } ) implies f1 = f2 )
assume that
A1: for x being Subset of R holds f1 . x = { u where u is Element of R : f . u meets x } and
A2: for x being Subset of R holds f2 . x = { u where u is Element of R : f . u meets x } ; :: thesis: f1 = f2
for y being Element of bool the carrier of R holds f1 . y = f2 . y

proof

let y be Element of bool the carrier of R; :: thesis: f1 . y = f2 . y
f1 . y = { u where u is Element of R : f . u meets y } by A1
.= f2 . y by A2 ;
hence f1 . y = f2 . y ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum