set li = right_closed_halfline 0;
let D, C be non empty set ; for F being PartFunc of D,REAL
for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
max- F, max- G are_fiberwise_equipotent
let F be PartFunc of D,REAL; for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
max- F, max- G are_fiberwise_equipotent
let G be PartFunc of C,REAL; ( F,G are_fiberwise_equipotent implies max- F, max- G are_fiberwise_equipotent )
assume A1:
F,G are_fiberwise_equipotent
; max- F, max- G are_fiberwise_equipotent
( rng (max- F) c= REAL & rng (max- G) c= REAL )
;
hence
max- F, max- G are_fiberwise_equipotent
by A2, CLASSES1:79; verum