deffunc H1( Subset of X, Subset of X) -> Element of NAT = card ($1 \+\ $2);
let f1, f2 be Function of [:(bool X),(bool X):],REAL; :: thesis: ( ( for x, y being Subset of X holds f1 . (x,y) = card (x \+\ y) ) & ( for x, y being Subset of X holds f2 . (x,y) = card (x \+\ y) ) implies f1 = f2 )
assume that
A1: for x, y being Subset of X holds f1 . (x,y) = H1(x,y) and
A2: for x, y being Subset of X holds f2 . (x,y) = H1(x,y) ; :: thesis: f1 = f2
for x being Element of [:(bool X),(bool X):] holds f1 . x = f2 . x
proof
let x be Element of [:(bool X),(bool X):]; :: thesis: f1 . x = f2 . x
consider x1, x2 being object such that
A3: [x1,x2] = x by XTUPLE_0:def 1, CARDFIL4:4;
reconsider x1 = x1, x2 = x2 as Subset of X by ZFMISC_1:87, A3;
A5: card (x1 \+\ x2) = f1 . (x1,x2) by A1
.= f1 . x by A3 ;
card (x1 \+\ x2) = f2 . (x1,x2) by A2
.= f2 . x by A3 ;
hence f1 . x = f2 . x by A5; :: thesis: verum
end;
hence f1 = f2 ; :: thesis: verum