let IIG be non empty non void Circuit-like ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
let SCS be non-empty Circuit of IIG; :: thesis: for s being State of SCS
for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
let s be State of SCS; :: thesis: for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
let o be OperSymbol of IIG; :: thesis: (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
A1: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
Result (o,SCS) = ( the Sorts of SCS * the ResultSort of IIG) . o by MSUALG_1:def 5
.= the Sorts of SCS . ( the ResultSort of IIG . o) by A1, FUNCT_1:13
.= the Sorts of SCS . (the_result_sort_of o) by MSUALG_1:def 2 ;
hence (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o) by FUNCT_2:5; :: thesis: verum