let D be non empty set ; :: thesis: for F being ManySortedFunction of
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st d in dom F & e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let F be ManySortedFunction of ; :: thesis: for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st d in dom F & e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let C be non empty functional with_common_domain set ; :: thesis: ( C = rng F implies for d being Element of D
for e being set st d in dom F & e in DOM C holds
(F . d) . e = ((commute F) . e) . d )
assume A1: C = rng F ; :: thesis: for d being Element of D
for e being set st d in dom F & e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let d be Element of D; :: thesis: for e being set st d in dom F & e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let e be set ; :: thesis: ( d in dom F & e in DOM C implies (F . d) . e = ((commute F) . e) . d )
assume A2: ( d in dom F & e in DOM C ) ; :: thesis: (F . d) . e = ((commute F) . e) . d
set E = union { (rng (F . d')) where d' is Element of D : verum } ;
reconsider F' = F as Function ;
A3: dom F' = D by PARTFUN1:def 4;
rng F' c= Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F' or x in Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } ) )
assume x in rng F' ; :: thesis: x in Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } )
then consider d' being set such that
A4: ( d' in dom F & F . d' = x ) by FUNCT_1:def 5;
reconsider d' = d' as Element of D by A4, PARTFUN1:def 4;
consider Fd being Function such that
A5: Fd = F . d' ;
F . d' in rng F by A4, FUNCT_1:def 5;
then A6: dom Fd = DOM C by A1, A5, CARD_3:def 12;
rng Fd c= union { (rng (F . d')) where d' is Element of D : verum }

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng Fd or x1 in union { (rng (F . d')) where d' is Element of D : verum } )
assume A7: x1 in rng Fd ; :: thesis: x1 in union { (rng (F . d')) where d' is Element of D : verum }
rng Fd in { (rng (F . d'')) where d'' is Element of D : verum } by A5;
hence x1 in union { (rng (F . d')) where d' is Element of D : verum } by A7, TARSKI:def 4; :: thesis: verum

end;

hence x in Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } ) by A4, A5, A6, FUNCT_2:def 2; :: thesis: verum

end;

then F in Funcs D,(Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } )) by A3, FUNCT_2:def 2;
hence (F . d) . e = ((commute F) . e) . d by A2, FUNCT_6:86; :: thesis: verum