theorem Th29: :: FLEXARY1:29

for n being Nat
for f1, f2 being natural-valued Function st n > 1 holds
( f1,f2 are_fiberwise_equipotent iff n |^ f1,n |^ f2 are_fiberwise_equipotent )