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