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

proof

let o be object ; :: 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 object 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 object 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] and
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₂[ object , object ] means ex D2 being set ex f being OperSymbol of A ex p being Element of P * st
( D2 = $2 & $1 = [f,p] & (Den (f,A)) .: (product p) c= D2 );
A3: for o being object 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 object st
( r in P & S₂[o,r] )

proof

let o be object ; :: 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 object 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 object 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] and
product p meets dom (Den (f,A)) ;
Den (f,A) is_exactly_partitable_wrt P by Def10;
then Den (f,A) is_partitable_wrt P ;
then ex a being Element of P st (Den (f,A)) .: (product p) c= a ;
hence ex r being object 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 object 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 FUNCT_1:sch 6(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:2;
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 object 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 FUNCT_1:sch 6(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:2;
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 A10: ex f1 being OperSymbol of A ex q1 being Element of P * st
( q1 = Ar . [f,p] & [f,p] = [f1,q1] ) by A6;
S₂[[f,p],R . [f,p]] by A8, A9;
then consider f2 being OperSymbol of A, q2 being Element of P * such that
A11: [f,p] = [f2,q2] and
A12: (Den (f2,A)) .: (product q2) c= R . [f,p] ;
q2 = p by A11, XTUPLE_0:1;
hence ( the Arity of S . [f,p] = p & (Den (f,A)) .: (product p) c= the ResultSort of S . [f,p] ) by A10, A11, A12, XTUPLE_0:1; :: thesis: verum