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:31 ;
:: thesis: verum