let I be set ; 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 ; 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; dom (uncurry (OPER A)) = [:I, the carrier' of S:]
per cases
( I <> {} or I = {} )
;
suppose A1:
I <> {}
;
dom (uncurry (OPER A)) = [:I, the carrier' of S:]thus
dom (uncurry (OPER A)) c= [:I, the carrier' of S:]
XBOOLE_0:def 10 [:I, the carrier' of S:] c= dom (uncurry (OPER A))proof
let t be
object ;
TARSKI:def 3 ( not t in dom (uncurry (OPER A)) or t in [:I, the carrier' of S:] )
assume
t in dom (uncurry (OPER A))
;
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;
verum
end; let x be
object ;
TARSKI:def 3 ( not x in [:I, the carrier' of S:] or x in dom (uncurry (OPER A)) )assume A6:
x in [:I, the carrier' of S:]
;
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;
verum end;