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