let A, B be non empty set ; :: thesis: for C, y being set
for f being Function st f in Funcs A,(Funcs B,C) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
let C, y be set ; :: thesis: for f being Function st f in Funcs A,(Funcs B,C) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
let f be Function; :: thesis: ( f in Funcs A,(Funcs B,C) & y in B implies ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) )
assume that
A1: f in Funcs A,(Funcs B,C) and
A2: y in B ; :: thesis: ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
set cf = commute f;
commute f in Funcs B,(Funcs A,C) by A1, FUNCT_6:85;
then A3: ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs A,C ) by FUNCT_2:def 2;
then (commute f) . y in rng (commute f) by A2, FUNCT_1:def 5;
then ex t being Function st
( t = (commute f) . y & dom t = A & rng t c= C ) by A3, FUNCT_2:def 2;
hence ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) ; :: thesis: verum