let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for o being OperSymbol of S st o = In (( the connectives of S . 3), the carrier' of S) holds
( o = the connectives of S . 3 & the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )
let o be OperSymbol of S; :: thesis: ( o = In (( the connectives of S . 3), the carrier' of S) implies ( o = the connectives of S . 3 & the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S ) )
assume A1: o = In (( the connectives of S . 3), the carrier' of S) ; :: thesis: ( o = the connectives of S . 3 & the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )
4 + 6 <= len the connectives of S by AOFA_A00:def 39;
then 3 <= len the connectives of S by XXREAL_0:2;
then 3 in dom the connectives of S by FINSEQ_3:25;
hence o = the connectives of S . 3 by A1, FUNCT_1:102, SUBSET_1:def 8; :: thesis: ( the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S )
then o is_of_type <* the bool-sort of S, the bool-sort of S*>, the bool-sort of S by AOFA_A00:def 31;
hence ( the_arity_of o = <* the bool-sort of S, the bool-sort of S*> & the_result_sort_of o = the bool-sort of S ) ; :: thesis: verum