let F1, F2 be Function of (the_subsets_of_card n,X),(the_subsets_of_card n,Y); :: thesis: ( ( for x being Element of the_subsets_of_card n,X holds F1 . x = f .: x ) & ( for x being Element of the_subsets_of_card n,X holds F2 . x = f .: x ) implies F1 = F2 )
assume that
A10: for x being Element of the_subsets_of_card n,X holds F1 . x = f .: x and
A11: for x being Element of the_subsets_of_card n,X holds F2 . x = f .: x ; :: thesis: F1 = F2

now

let x be set ; :: thesis: ( x in the_subsets_of_card n,X implies F1 . x = F2 . x )
assume x in the_subsets_of_card n,X ; :: thesis: F1 . x = F2 . x
then reconsider x9 = x as Element of the_subsets_of_card n,X ;
thus F1 . x = f .: x9 by A10
.= F2 . x by A11 ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:18; :: thesis: verum