let F, G be Function; ( 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
; 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 ; ( 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
; 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; verum