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₁ being set st b₁ = g `2 holds
( b₁ is Function-like & b₁ is Relation-like ) ; :: thesis: verum