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 9 :: thesis: ^ = ^
thus IT1 . x = (LO ^ s) .: x by A19
.= IT2 . x by A20 ; :: thesis: verum