set EE = the_subsets_of_card (n,E);
let IT1, IT2 be Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)); :: thesis: ( ( for X being Element of the_subsets_of_card (n,E) holds IT1 . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card (n,E) holds IT2 . X = (LO ^ s) .: X ) implies IT1 = IT2 )
assume that
A19: for X being Element of the_subsets_of_card (n,E) holds IT1 . X = (LO ^ s) .: X and
A20: for X being Element of the_subsets_of_card (n,E) holds IT2 . X = (LO ^ s) .: X ; :: thesis: IT1 = IT2
let x be Element of the_subsets_of_card (n,E); :: according to FUNCT_2:def 8 :: thesis: ^ = ^
thus IT1 . x = (LO ^ s) .: x by A19
.= IT2 . x by A20 ; :: thesis: verum