let X be finite set ; for Fy being finite-yielding Function
for x being object st Fy = x .--> X holds
Card_Intersection (Fy,1) = card X
let Fy be finite-yielding Function; for x being object st Fy = x .--> X holds
Card_Intersection (Fy,1) = card X
let x be object ; ( Fy = x .--> X implies Card_Intersection (Fy,1) = card X )
assume A1:
Fy = x .--> X
; Card_Intersection (Fy,1) = card X
then A2:
dom Fy = {x}
;
A3:
x in {x}
by TARSKI:def 1;
then A4:
(x .--> x) " {x} = {x}
by FUNCOP_1:14;
Fy . x = X
by A1, A3, FUNCOP_1:7;
then
( 1 = card {x} & Intersection (Fy,(x .--> x),x) = X )
by A4, Th34, CARD_1:30;
hence
Card_Intersection (Fy,1) = card X
by A2, Th44; verum