let S1 be non empty non void ManySortedSign ; :: thesis: for S2 being non empty ManySortedSign st S1 tolerates S2 holds
for o1 being OperSymbol of S1
for o being OperSymbol of (S1 +* S2) st o1 = o holds
( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )
let S2 be non empty ManySortedSign ; :: thesis: ( S1 tolerates S2 implies for o1 being OperSymbol of S1
for o being OperSymbol of (S1 +* S2) st o1 = o holds
( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 ) )
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def 1 :: thesis: for o1 being OperSymbol of S1
for o being OperSymbol of (S1 +* S2) st o1 = o holds
( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )
let o1 be OperSymbol of S1; :: thesis: for o being OperSymbol of (S1 +* S2) st o1 = o holds
( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )
let o be OperSymbol of (S1 +* S2); :: thesis: ( o1 = o implies ( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 ) )
assume A3: o1 = o ; :: thesis: ( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )
A4: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by Def2;
hence the_arity_of o = the_arity_of o1 by A1, A3, A4, FUNCT_4:15; :: thesis: the_result_sort_of o = the_result_sort_of o1
A5: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by Def2;
hence the_result_sort_of o = the_result_sort_of o1 by A2, A3, A5, FUNCT_4:15; :: thesis: verum