reconsider X9 = X as SetWithCompoundTerm of S,V by A1;
reconsider o9 = o as Gate of (X9 -CircuitStr) ;
take the Charact of A . ((o9 . {}) `1) ; :: thesis: for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
the Charact of A . ((o9 . {}) `1) = the Charact of A . ((o9 . {}) `1)
thus for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
the Charact of A . ((o9 . {}) `1) = the Charact of A . ((o9 . {}) `1) ; :: thesis: verum