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