let I be set ; :: thesis: for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]
let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]
let A be MSAlgebra-Family of I,S; :: thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:]

per cases ( I <> {} or I = {} ) ;

suppose A1: I <> {} ; :: thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:]

thus dom (uncurry (OPER A)) c= [:I, the carrier' of S:] :: according to XBOOLE_0:def 10 :: thesis: [:I, the carrier' of S:] c= dom (uncurry (OPER A))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in dom (uncurry (OPER A)) or t in [:I, the carrier' of S:] )
assume t in dom (uncurry (OPER A)) ; :: thesis: t in [:I, the carrier' of S:]
then consider x being object , g being Function, y being object such that
A2: t = [x,y] and
A3: x in dom (OPER A) and
A4: ( g = (OPER A) . x & y in dom g ) by FUNCT_5:def 2;
reconsider x = x as Element of I by A3, PARTFUN1:def 2;
ex U0 being MSAlgebra over S st
( U0 = A . x & (OPER A) . x = the Charact of U0 ) by A1, Def11;
then A5: y in the carrier' of S by A4, PARTFUN1:def 2;
x in I by A3, PARTFUN1:def 2;
hence t in [:I, the carrier' of S:] by A2, A5, ZFMISC_1:87; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:I, the carrier' of S:] or x in dom (uncurry (OPER A)) )
assume A6: x in [:I, the carrier' of S:] ; :: thesis: x in dom (uncurry (OPER A))
then consider y, z being object such that
A7: x = [y,z] by RELAT_1:def 1;
A8: z in the carrier' of S by A6, A7, ZFMISC_1:87;
reconsider y = y as Element of I by A6, A7, ZFMISC_1:87;
consider U0 being MSAlgebra over S such that
U0 = A . y and
A9: (OPER A) . y = the Charact of U0 by A1, Def11;
( dom the Charact of U0 = the carrier' of S & dom (OPER A) = I ) by PARTFUN1:def 2;
hence x in dom (uncurry (OPER A)) by A1, A7, A8, A9, FUNCT_5:def 2; :: thesis: verum

end;

suppose A10: I = {} ; :: thesis: dom (uncurry (OPER A)) = [:I, the carrier' of S:]

then OPER A = {} ;
hence dom (uncurry (OPER A)) = [:I, the carrier' of S:] by A10, FUNCT_5:43, RELAT_1:38, ZFMISC_1:90; :: thesis: verum

end;

end;