let S1 be non empty ManySortedSign ; :: thesis: for S2 being non empty non void ManySortedSign
for o2 being OperSymbol of S2
for o being OperSymbol of (S1 +* S2) st o2 = o holds
( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )
let S2 be non empty non void ManySortedSign ; :: thesis: for o2 being OperSymbol of S2
for o being OperSymbol of (S1 +* S2) st o2 = o holds
( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )
let o2 be OperSymbol of S2; :: thesis: for o being OperSymbol of (S1 +* S2) st o2 = o holds
( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )
let o be OperSymbol of (S1 +* S2); :: thesis: ( o2 = o implies ( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 ) )
assume A1: o2 = o ; :: thesis: ( the_arity_of o = the_arity_of o2 & the_result_sort_of o = the_result_sort_of o2 )
A2: dom the Arity of S2 = the carrier' of S2 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 o2 by A1, A2, FUNCT_4:13; :: thesis: the_result_sort_of o = the_result_sort_of o2
A3: dom the ResultSort of S2 = the carrier' of S2 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 o2 by A1, A3, FUNCT_4:13; :: thesis: verum