let f1, f2 be Function; :: thesis: ( ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f2 = the Charact of A . ((o9 . {}) `1) ) implies f1 = f2 )
reconsider X9 = X as SetWithCompoundTerm of S,V by A1;
reconsider o9 = o as Gate of (X9 -CircuitStr) ;
assume A2: ( ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds
for o9 being Gate of (X9 -CircuitStr) st o9 = o holds
f2 = the Charact of A . ((o9 . {}) `1) ) & not f1 = f2 ) ; :: thesis: contradiction
then f1 = the Charact of A . ((o9 . {}) `1) ;
hence contradiction by A2; :: thesis: verum