consider A being MSAlgebra over S such that

A1: A is gate`2=den by CIRCCOMB:def 11;

g `2 = [(g `1),( the Charact of A . g)] `2 by A1

.= the Charact of A . g

.= Den (g,A) by MSUALG_1:def 6 ;

hence for b_{1} being set st b_{1} = g `2 holds

( b_{1} is Function-like & b_{1} is Relation-like )
; :: thesis: verum

A1: A is gate`2=den by CIRCCOMB:def 11;

g `2 = [(g `1),( the Charact of A . g)] `2 by A1

.= the Charact of A . g

.= Den (g,A) by MSUALG_1:def 6 ;

hence for b

( b