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)); ( ( 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
; IT1 = IT2
let x be Element of the_subsets_of_card (n,E); FUNCT_2:def 8 ^ = ^
thus IT1 . x =
(LO ^ s) .: x
by A19
.=
IT2 . x
by A20
; verum