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:55;
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 3;
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