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
set ;
:: 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
set ,
g being
Function,
y being
set such that A2:
(
t = [x,y] &
x in dom (OPER A) &
g = (OPER A) . x &
y in dom g )
by FUNCT_5:def 4;
reconsider x =
x as
Element of
I by A2, PARTFUN1:def 4;
consider U0 being
MSAlgebra of
S such that A3:
(
U0 = A . x &
(OPER A) . x = the
Charact of
U0 )
by A1, Def18;
(
x in I &
y in the
carrier' of
S )
by A2, A3, PARTFUN1:def 4;
hence
t in [:I,the carrier' of S:]
by A2, ZFMISC_1:106;
:: thesis: verum
end; let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in [:I,the carrier' of S:] or x in dom (uncurry (OPER A)) )assume A4:
x in [:I,the carrier' of S:]
;
:: thesis: x in dom (uncurry (OPER A))then consider y,
z being
set such that A5:
x = [y,z]
by RELAT_1:def 1;
reconsider y =
y as
Element of
I by A4, A5, ZFMISC_1:106;
A6:
z in the
carrier' of
S
by A4, A5, ZFMISC_1:106;
consider U0 being
MSAlgebra of
S such that A7:
(
U0 = A . y &
(OPER A) . y = the
Charact of
U0 )
by A1, Def18;
A8:
dom the
Charact of
U0 = the
carrier' of
S
by PARTFUN1:def 4;
dom (OPER A) = I
by PARTFUN1:def 4;
hence
x in dom (uncurry (OPER A))
by A1, A5, A6, A7, A8, FUNCT_5:def 4;
:: thesis: verum end;