let I be non empty set ; 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 ; 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; 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; 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 Th5;
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:90;
hence
commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
by FUNCT_6:10; verum