let x be set ; for S being non empty strict ManySortedSign
for A being Boolean MSAlgebra of 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 of 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 of 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 Th5;
A3:
{x} c= the carrier of S
by A1, ZFMISC_1:37;
A4:
the carrier of (SingleMSS x) = {x}
by Def1;
A5:
the Sorts of A = the carrier of S --> BOOLEAN
by CIRCCOMB:65;
the Sorts of (SingleMSA x) = the carrier of (SingleMSS x) --> BOOLEAN
by CIRCCOMB:65;
then A6:
the Sorts of (SingleMSA x) tolerates the Sorts of A
by A5, CIRCCOMB:4;
dom the Charact of (SingleMSA x) = {}
by PARTFUN1:def 4;
then
the Charact of (SingleMSA x) = {}
;
then A7:
the Charact of A = the Charact of (SingleMSA x) +* the Charact of A
by FUNCT_4:21;
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 4;
dom the Sorts of A = the carrier of S
by PARTFUN1:def 4;
hence
(SingleMSA x) +* A = MSAlgebra(# the Sorts of A,the Charact of A #)
by A2, A3, A4, A8, A9, A10, FUNCT_4:20; verum