let x be set ; for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra over S st x in the carrier of S holds
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
let S be non empty strict ManySortedSign ; for A being Boolean MSAlgebra over S st x in the carrier of S holds
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be Boolean MSAlgebra over S; ( x in the carrier of S implies (SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #) )
set S1 = SingleMSS x;
set A1 = SingleMSA x;
assume A1:
x in the carrier of S
; (SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
then A2:
(SingleMSS x) +* S = S
by Th4;
A3:
{x} c= the carrier of S
by A1, ZFMISC_1:31;
A4:
the carrier of (SingleMSS x) = {x}
by Def1;
A5:
the Sorts of A = the carrier of S --> BOOLEAN
by CIRCCOMB:57;
the Sorts of (SingleMSA x) = the carrier of (SingleMSS x) --> BOOLEAN
by CIRCCOMB:57;
then A6:
the Sorts of (SingleMSA x) tolerates the Sorts of A
by A5, FUNCOP_1:87;
A7:
the Charact of A = the Charact of (SingleMSA x) +* the Charact of A
;
A8:
the Sorts of ((SingleMSA x) +* A) = the Sorts of (SingleMSA x) +* the Sorts of A
by A6, CIRCCOMB:def 4;
A9:
the Charact of A = the Charact of ((SingleMSA x) +* A)
by A6, A7, CIRCCOMB:def 4;
A10:
dom the Sorts of (SingleMSA x) = the carrier of (SingleMSS x)
by PARTFUN1:def 2;
dom the Sorts of A = the carrier of S
by PARTFUN1:def 2;
hence
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
by A2, A3, A4, A8, A9, A10, FUNCT_4:19; verum