deffunc H₁( Subset of X, Subset of X) -> Element of REAL = In ((card ($1 \+\ $2)),REAL);
ex f being Function of [:(bool X),(bool X):],REAL st
for x, y being Element of bool X holds f . (x,y) = H₁(x,y) from STACKS_1:sch 2();
then consider f being Function of [:(bool X),(bool X):],REAL such that
A1: for x, y being Subset of X holds f . (x,y) = H₁(x,y) ;
take f ; :: thesis: for x, y being Subset of X holds f . (x,y) = card (x \+\ y)
let x, y be Subset of X; :: thesis: f . (x,y) = card (x \+\ y)
f . (x,y) = In ((card (x \+\ y)),REAL) by A1
.= card (x \+\ y) ;
hence f . (x,y) = card (x \+\ y) ; :: thesis: verum