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 A1: S = 1GateCircStr p,x ; :: thesis: Output S = [p,x]
thus Output S = union {[p,x]} by A1, CIRCCOMB:def 6
.= [p,x] by ZFMISC_1:31 ; :: thesis: verum