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

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 :: thesis: for x being object st x in the_subsets_of_card (n,X) holds

F1 . x = F2 . x

hence
F1 = F2
by FUNCT_2:12; :: thesis: verumF1 . x = F2 . x

let x be object ; :: 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;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