let S be 1-sorted ; :: thesis: for T being non empty 1-sorted
for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X ` )
let T be non empty 1-sorted ; :: thesis: for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X ` )
let f be Function of S,T; :: thesis: for X being Subset of T holds (f " X) ` = f " (X ` )
let X be Subset of T; :: thesis: (f " X) ` = f " (X ` )
thus (f " X) ` = the carrier of S \ (f " X) by SUBSET_1:def 5
.= (f " the carrier of T) \ (f " X) by FUNCT_2:48
.= f " (the carrier of T \ X) by FUNCT_1:138
.= f " (X ` ) by SUBSET_1:def 5 ; :: thesis: verum