let S be one-gate ManySortedSign ; :: thesis: for p being FinSequence
for x being set st S = 1GateCircStr (p,x) holds
Output S = [p,x]
let p be FinSequence; :: thesis: for x being set st S = 1GateCircStr (p,x) holds
Output S = [p,x]
let x be set ; :: thesis: ( S = 1GateCircStr (p,x) implies Output S = [p,x] )
assume S = 1GateCircStr (p,x) ; :: thesis: Output S = [p,x]
hence Output S = union {[p,x]} by CIRCCOMB:def 6
.= [p,x] by ZFMISC_1:25 ;
:: thesis: verum