let x be set ; :: thesis: for X being finite set
for Fy being finite-yielding Function st Fy = x .--> X holds
Card_Intersection (Fy,1) = card X
let X be finite set ; :: thesis: for Fy being finite-yielding Function st Fy = x .--> X holds
Card_Intersection (Fy,1) = card X
let Fy be finite-yielding Function; :: 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} by FUNCOP_1:13;
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, Th37, CARD_1:30;
hence Card_Intersection (Fy,1) = card X by A2, Th53; :: thesis: verum