set O = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ;
defpred S₁[ set , set ] means ex f being OperSymbol of A ex q being Element of P * st
( q = $2 & $1 = [f,q] );
A1: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } holds
ex p being set st
( p in P * & S₁[o,p] )

proof

let o be set ; :: thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } implies ex p being set st
( p in P * & S₁[o,p] ) )
assume o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ; :: thesis: ex p being set st
( p in P * & S₁[o,p] )
then consider f being OperSymbol of A, p being Element of P * such that
A2: ( o = [f,p] & product p meets dom (Den f,A) ) ;
take p ; :: thesis: ( p in P * & S₁[o,p] )
thus ( p in P * & S₁[o,p] ) by A2; :: thesis: verum

end;

defpred S₂[ set , set ] means ex f being OperSymbol of A ex p being Element of P * st
( $1 = [f,p] & (Den f,A) .: (product p) c= $2 );
A3: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } holds
ex r being set st
( r in P & S₂[o,r] )

proof

let o be set ; :: thesis: ( o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } implies ex r being set st
( r in P & S₂[o,r] ) )
assume o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ; :: thesis: ex r being set st
( r in P & S₂[o,r] )
then consider f being OperSymbol of A, p being Element of P * such that
A4: ( o = [f,p] & product p meets dom (Den f,A) ) ;
Den f,A is_exactly_partitable_wrt P by Def11;
then Den f,A is_partitable_wrt P by Def10;
then ex a being Element of P st (Den f,A) .: (product p) c= a by Def9;
hence ex r being set st
( r in P & S₂[o,r] ) by A4; :: thesis: verum

end;

consider Ar being Function such that
A5: ( dom Ar = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } & rng Ar c= P * ) and
A6: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } holds
S₁[o,Ar . o] from WELLORD2:sch 1(A1);
reconsider Ar = Ar as Function of { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ,(P * ) by A5, FUNCT_2:4;
consider R being Function such that
A7: ( dom R = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } & rng R c= P ) and
A8: for o being set st o in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } holds
S₂[o,R . o] from WELLORD2:sch 1(A3);
reconsider R = R as Function of { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ,P by A7, FUNCT_2:4;
take S = ManySortedSign(# P,{ [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ,Ar,R #); :: thesis: ( the carrier of S = P & the carrier' of S = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den o,A) } & ( for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den o,A) holds
( the Arity of S . [o,p] = p & (Den o,A) .: (product p) c= the ResultSort of S . [o,p] ) ) )
thus ( the carrier of S = P & the carrier' of S = { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ) ; :: thesis: for o being OperSymbol of A
for p being Element of P * st product p meets dom (Den o,A) holds
( the Arity of S . [o,p] = p & (Den o,A) .: (product p) c= the ResultSort of S . [o,p] )
let f be OperSymbol of A; :: thesis: for p being Element of P * st product p meets dom (Den f,A) holds
( the Arity of S . [f,p] = p & (Den f,A) .: (product p) c= the ResultSort of S . [f,p] )
let p be Element of P * ; :: thesis: ( product p meets dom (Den f,A) implies ( the Arity of S . [f,p] = p & (Den f,A) .: (product p) c= the ResultSort of S . [f,p] ) )
set o = [f,p];
assume product p meets dom (Den f,A) ; :: thesis: ( the Arity of S . [f,p] = p & (Den f,A) .: (product p) c= the ResultSort of S . [f,p] )
then A9: [f,p] in { [f,p] where f is OperSymbol of A, p is Element of P * : product p meets dom (Den f,A) } ;
then consider f1 being OperSymbol of A, q1 being Element of P * such that
A10: ( q1 = Ar . [f,p] & [f,p] = [f1,q1] ) by A6;
consider f2 being OperSymbol of A, q2 being Element of P * such that
A11: ( [f,p] = [f2,q2] & (Den f2,A) .: (product q2) c= R . [f,p] ) by A8, A9;
( q1 = p & q2 = p & f2 = f ) by A10, A11, ZFMISC_1:33;
hence ( the Arity of S . [f,p] = p & (Den f,A) .: (product p) c= the ResultSort of S . [f,p] ) by A10, A11; :: thesis: verum