let X be non-empty 1 -element FinSequence; :: thesis: for S being SemiringFamily of X holds SemiringProduct S = { (product <*s*>) where s is Element of S . 1 : verum }
let S be SemiringFamily of X; :: thesis: SemiringProduct S = { (product <*s*>) where s is Element of S . 1 : verum }
A1: dom X = {1} by FINSEQ_1:2, FINSEQ_1:89;
A2: S is non-empty

proof

assume not S is non-empty ; :: thesis: contradiction
then {} in rng S by RELAT_1:def 9;
then consider a being object such that
A3: a in dom S and
A4: S . a = {} by FUNCT_1:def 3;
a in dom X by Thm16, A3;
then A5: S . 1 = {} by A4, A1, TARSKI:def 1;
( S is SemiringFamily of X & 1 in Seg 1 ) by FINSEQ_1:3;
hence contradiction by A5, Def2; :: thesis: verum

end;

then A6: product S = { <*s*> where s is Element of S . 1 : verum } by Thm21;

now :: thesis: ( ( for x being object st x in SemiringProduct S holds
x in { (product <*s*>) where s is Element of S . 1 : verum } ) & ( for x being object st x in { (product <*s*>) where s is Element of S . 1 : verum } holds
x in SemiringProduct S ) )

hereby :: thesis: for x being object st x in { (product <*s*>) where s is Element of S . 1 : verum } holds
x in SemiringProduct S

let x be object ; :: thesis: ( x in SemiringProduct S implies x in { (product <*s*>) where s is Element of S . 1 : verum } )
assume x in SemiringProduct S ; :: thesis: x in { (product <*s*>) where s is Element of S . 1 : verum }
then consider f being Function such that
A7: x = product f and
A8: f in product S by Def3;
f in { <*s*> where s is Element of S . 1 : verum } by A2, A8, Thm21;
then consider s being Element of S . 1 such that
A9: f = <*s*> ;
thus x in { (product <*s*>) where s is Element of S . 1 : verum } by A7, A9; :: thesis: verum

end;

let x be object ; :: thesis: ( x in { (product <*s*>) where s is Element of S . 1 : verum } implies x in SemiringProduct S )
assume x in { (product <*s*>) where s is Element of S . 1 : verum } ; :: thesis: x in SemiringProduct S
then consider s being Element of S . 1 such that
A10: x = product <*s*> ;
set f = <*s*>;
( x = product <*s*> & <*s*> in product S ) by A10, A6;
hence x in SemiringProduct S by Def3; :: thesis: verum

end;

then ( { (product <*s*>) where s is Element of S . 1 : verum } c= SemiringProduct S & SemiringProduct S c= { (product <*s*>) where s is Element of S . 1 : verum } ) ;
hence SemiringProduct S = { (product <*s*>) where s is Element of S . 1 : verum } ; :: thesis: verum