let D be non empty set ; for F, G being Function st rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim F,d) = card (Coim G,d) ) holds
F,G are_fiberwise_equipotent
let F, G be Function; ( rng F c= D & rng G c= D & ( for d being Element of D holds card (Coim F,d) = card (Coim G,d) ) implies F,G are_fiberwise_equipotent )
assume that
A1:
rng F c= D
and
A2:
rng G c= D
; ( ex d being Element of D st not card (Coim F,d) = card (Coim G,d) or F,G are_fiberwise_equipotent )
assume A3:
for d being Element of D holds card (Coim F,d) = card (Coim G,d)
; F,G are_fiberwise_equipotent
let x be set ; CLASSES1:def 9 card (Coim F,x) = card (Coim G,x)
per cases
( not x in rng F or x in rng F )
;
suppose A4:
not
x in rng F
;
card (Coim F,x) = card (Coim G,x)A5:
Coim F,
x = {}
by A4, Lm3;
A6:
now assume A7:
x in rng G
;
contradictionreconsider d =
x as
Element of
D by A2, A7;
A8:
card (Coim G,d) = card (Coim F,d)
by A3;
A9:
G " {d},
F " {d} are_equipotent
by A8, CARD_1:21;
A10:
G " {x} = {}
by A5, A9, CARD_1:46;
consider y being
set such that A11:
y in dom G
and A12:
G . y = x
by A7, FUNCT_1:def 5;
A13:
G . y in {x}
by A12, TARSKI:def 1;
thus
contradiction
by A10, A11, A13, FUNCT_1:def 13;
verum end; thus
card (Coim F,x) = card (Coim G,x)
by A5, A6, Lm3;
verum end;