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:19;
A3: x in {x} by TARSKI:def 1;
then A4: (x .--> x) " {x} = {x} by FUNCOP_1:20;
Fy . x = X by A1, A3, FUNCOP_1:13;
then ( 1 = card {x} & Intersection Fy,(x .--> x),x = X ) by A4, Th37, CARD_1:50;
hence Card_Intersection Fy,1 = card X by A2, Th53; :: thesis: verum