let F, G be Function; :: thesis: ( F,G are_fiberwise_equipotent implies for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds

ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) )

assume F,G are_fiberwise_equipotent ; :: thesis: for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds

ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )

then consider H being Function such that

A1: dom H = dom F and

A2: rng H = dom G and

A3: H is one-to-one and

A4: F = G * H by CLASSES1:77;

let x1, x2 be set ; :: thesis: ( x1 in dom F & x2 in dom F & x1 <> x2 implies ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) )

assume that

A5: x1 in dom F and

A6: x2 in dom F and

A7: x1 <> x2 ; :: thesis: ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )

A8: ( H . x1 in dom G & H . x2 in dom G ) by A5, A6, A1, A2, FUNCT_1:3;

A9: F . x2 = G . (H . x2) by A6, A4, FUNCT_1:12;

( H . x1 <> H . x2 & F . x1 = G . (H . x1) ) by A5, A6, A7, A1, A3, A4, FUNCT_1:12, FUNCT_1:def 4;

hence ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by A8, A9; :: thesis: verum

ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) )

assume F,G are_fiberwise_equipotent ; :: thesis: for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds

ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )

then consider H being Function such that

A1: dom H = dom F and

A2: rng H = dom G and

A3: H is one-to-one and

A4: F = G * H by CLASSES1:77;

let x1, x2 be set ; :: thesis: ( x1 in dom F & x2 in dom F & x1 <> x2 implies ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) )

assume that

A5: x1 in dom F and

A6: x2 in dom F and

A7: x1 <> x2 ; :: thesis: ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )

A8: ( H . x1 in dom G & H . x2 in dom G ) by A5, A6, A1, A2, FUNCT_1:3;

A9: F . x2 = G . (H . x2) by A6, A4, FUNCT_1:12;

( H . x1 <> H . x2 & F . x1 = G . (H . x1) ) by A5, A6, A7, A1, A3, A4, FUNCT_1:12, FUNCT_1:def 4;

hence ex z1, z2 being set st

( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by A8, A9; :: thesis: verum