let X, a, b be set ; :: thesis: for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})
let f be Function of X,{a,b}; :: thesis: X = (f " {a}) \/ (f " {b})
thus X = f " {a,b} by FUNCT_2:40
.= f " ({a} \/ {b}) by ENUMSET1:1
.= (f " {a}) \/ (f " {b}) by RELAT_1:140 ; :: thesis: verum