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

let x be set ; :: 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 & C2 . o = the_action_of o,A ) by A1, A2, A3;
hence C1 . x = C2 . x ; :: thesis: verum

end;

hence C1 = C2 by PBOOLE:3; :: thesis: verum