let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs the carrier' of S,(Funcs I,(rng (uncurry (OPER A))))
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs the carrier' of S,(Funcs I,(rng (uncurry (OPER A))))
let A be MSAlgebra-Family of I,S; :: thesis: for o being OperSymbol of S holds commute (OPER A) in Funcs the carrier' of S,(Funcs I,(rng (uncurry (OPER A))))
let o be OperSymbol of S; :: thesis: commute (OPER A) in Funcs the carrier' of S,(Funcs I,(rng (uncurry (OPER A))))
set f = uncurry (OPER A);
dom (uncurry (OPER A)) = [:I,the carrier' of S:] by Th12;
then ( [:I,the carrier' of S:] <> {} & uncurry (OPER A) in Funcs [:I,the carrier' of S:],(rng (uncurry (OPER A))) ) by FUNCT_2:def 2, ZFMISC_1:113;
hence commute (OPER A) in Funcs the carrier' of S,(Funcs I,(rng (uncurry (OPER A)))) by FUNCT_6:19; :: thesis: verum