let C1, C2 be ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr); :: thesis: ( ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
C1 . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
C2 . g = the_action_of (g,A) ) implies C1 = C2 )
assume that
A1: for o being Gate of (X -CircuitStr) st o in the carrier' of (X -CircuitStr) holds
C1 . o = the_action_of (o,A) and
A2: for o being Gate of (X -CircuitStr) st o in the carrier' of (X -CircuitStr) holds
C2 . o = the_action_of (o,A) ; :: thesis: C1 = C2

now :: thesis: for x being object st x in the carrier' of (X -CircuitStr) holds
C1 . x = C2 . x

let x be object ; :: thesis: ( x in the carrier' of (X -CircuitStr) implies C1 . x = C2 . x )
assume A3: x in the carrier' of (X -CircuitStr) ; :: thesis: C1 . x = C2 . x
then reconsider o = x as Gate of (X -CircuitStr) ;
C1 . o = the_action_of (o,A) by A1, A3;
hence C1 . x = C2 . x by A2, A3; :: thesis: verum

end;

hence C1 = C2 ; :: thesis: verum