let D, C be non empty set ; :: thesis: for F being PartFunc of D,REAL
for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
abs F, abs G are_fiberwise_equipotent
let F be PartFunc of D,REAL; :: thesis: for G being PartFunc of C,REAL st F,G are_fiberwise_equipotent holds
abs F, abs G are_fiberwise_equipotent
let G be PartFunc of C,REAL; :: thesis: ( F,G are_fiberwise_equipotent implies abs F, abs G are_fiberwise_equipotent )
assume A1: F,G are_fiberwise_equipotent ; :: thesis: abs F, abs G are_fiberwise_equipotent

A2: now :: thesis: for r being Element of REAL holds card (Coim ((abs F),r)) = card (Coim ((abs G),r))

let r be Element of REAL ; :: thesis: card (Coim ((abs F),r)) = card (Coim ((abs G),r))

now :: thesis: ( ( 0 < r & card ((abs F) " {r}) = card ((abs G) " {r}) ) or ( 0 = r & card ((abs F) " {r}) = card ((abs G) " {r}) ) or ( r < 0 & card ((abs F) " {r}) = card ((abs G) " {r}) ) )

per cases ( 0 < r or 0 = r or r < 0 ) ;

case 0 < r ; :: thesis: card ((abs F) " {r}) = card ((abs G) " {r})

then ( (abs F) " {r} = F " {(- r),r} & (abs G) " {r} = G " {(- r),r} ) by Th8;
hence card ((abs F) " {r}) = card ((abs G) " {r}) by A1, CLASSES1:78; :: thesis: verum

end;

case 0 = r ; :: thesis: card ((abs F) " {r}) = card ((abs G) " {r})

then ( (abs F) " {r} = F " {r} & (abs G) " {r} = G " {r} ) by Th9;
hence card ((abs F) " {r}) = card ((abs G) " {r}) by A1, CLASSES1:78; :: thesis: verum

end;

case A3: r < 0 ; :: thesis: card ((abs F) " {r}) = card ((abs G) " {r})

then (abs F) " {r} = {} by Th10;
hence card ((abs F) " {r}) = card ((abs G) " {r}) by A3, Th10; :: thesis: verum

end;

end;

end;

hence card (Coim ((abs F),r)) = card (Coim ((abs G),r)) ; :: thesis: verum

end;

( rng (abs F) c= REAL & rng (abs G) c= REAL ) ;
hence abs F, abs G are_fiberwise_equipotent by A2, CLASSES1:79; :: thesis: verum