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 A1: 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 )
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
A2: x1 in dom F and
A3: x2 in dom F and
A4: 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 )
consider H being Function such that
A5: ( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) by A1, CLASSES1:85;
A6: ( H . x1 in dom G & H . x2 in dom G ) by A2, A3, A5, FUNCT_1:12;
A7: H . x1 <> H . x2 by A2, A3, A4, A5, FUNCT_1:def 8;
( F . x1 = G . (H . x1) & F . x2 = G . (H . x2) ) by A2, A3, A5, FUNCT_1:22;
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 A6, A7; :: thesis: verum