let X be finite set ; :: thesis: 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; :: thesis: for x being object st Fy = x .--> X holds
Card_Intersection (Fy,1) = card X
let x be object ; :: thesis: ( Fy = x .--> X implies Card_Intersection (Fy,1) = card X )
assume A1: Fy = x .--> X ; :: thesis: 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; :: thesis: verum