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