let f, g be Function; :: thesis: ( rng f = rng g & f is one-to-one & g is one-to-one implies f,g are_fiberwise_equipotent )

assume that

A1: rng f = rng g and

A2: f is one-to-one and

A3: g is one-to-one ; :: thesis: f,g are_fiberwise_equipotent

let x be object ; :: according to CLASSES1:def 10 :: thesis: card (Coim (f,x)) = card (Coim (g,x))

assume that

A1: rng f = rng g and

A2: f is one-to-one and

A3: g is one-to-one ; :: thesis: f,g are_fiberwise_equipotent

let x be object ; :: according to CLASSES1:def 10 :: thesis: card (Coim (f,x)) = card (Coim (g,x))