let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for x being set st x in (((Class R) # ) * the Arity of S) . o holds
ex a being Element of Args o,A st x = R # a
let o be OperSymbol of S; :: thesis: for A being non-empty MSAlgebra of S
for R being MSCongruence of A
for x being set st x in (((Class R) # ) * the Arity of S) . o holds
ex a being Element of Args o,A st x = R # a
let A be non-empty MSAlgebra of S; :: thesis: for R being MSCongruence of A
for x being set st x in (((Class R) # ) * the Arity of S) . o holds
ex a being Element of Args o,A st x = R # a
let R be MSCongruence of A; :: thesis: for x being set st x in (((Class R) # ) * the Arity of S) . o holds
ex a being Element of Args o,A st x = R # a
let x be set ; :: thesis: ( x in (((Class R) # ) * the Arity of S) . o implies ex a being Element of Args o,A st x = R # a )
assume A1: x in (((Class R) # ) * the Arity of S) . o ; :: thesis: ex a being Element of Args o,A st x = R # a
set ar = the_arity_of o;
A2: the_arity_of o = the Arity of S . o by MSUALG_1:def 6;
then (((Class R) # ) * the Arity of S) . o = product ((Class R) * (the_arity_of o)) by MSAFREE:1;
then consider f being Function such that
A3: f = x and
A4: dom f = dom ((Class R) * (the_arity_of o)) and
A5: for y being set st y in dom ((Class R) * (the_arity_of o)) holds
f . y in ((Class R) * (the_arity_of o)) . y by A1, CARD_3:def 5;
defpred S₁[ set , set ] means $2 in f . $1;
A6: dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 4;
A7: for n being Nat st n in dom f holds
f . n in Class (R . ((the_arity_of o) /. n))

proof

let n be Nat; :: thesis: ( n in dom f implies f . n in Class (R . ((the_arity_of o) /. n)) )
reconsider s = (the_arity_of o) /. n as Element of S ;
assume A8: n in dom f ; :: thesis: f . n in Class (R . ((the_arity_of o) /. n))
then (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, PARTFUN1:def 8;
then ((Class R) * (the_arity_of o)) . n = (Class R) . s by A4, A8, FUNCT_1:22
.= Class (R . s) by Def8 ;
hence f . n in Class (R . ((the_arity_of o) /. n)) by A4, A5, A8; :: thesis: verum

end;

A9: for a being set st a in dom f holds
ex b being set st S₁[a,b]

proof

let a be set ; :: thesis: ( a in dom f implies ex b being set st S₁[a,b] )
reconsider s = (the_arity_of o) /. a as Element of S ;
assume A10: a in dom f ; :: thesis: ex b being set st S₁[a,b]
then reconsider n = a as Nat by A4, A6, ORDINAL1:def 13;
f . n in Class (R . s) by A7, A10;
then consider a1 being set such that
A11: ( a1 in the Sorts of A . s & f . n = Class (R . s),a1 ) by EQREL_1:def 5;
take a1 ; :: thesis: S₁[a,a1]
thus S₁[a,a1] by A11, EQREL_1:28; :: thesis: verum

end;

consider g being Function such that
A12: ( dom g = dom f & ( for a being set st a in dom f holds
S₁[a,g . a] ) ) from CLASSES1:sch 1(A9);
dom the Sorts of A = the carrier of S by PARTFUN1:def 4;
then rng (the_arity_of o) c= dom the Sorts of A ;
then A13: dom g = dom (the Sorts of A * (the_arity_of o)) by A4, A6, A12, RELAT_1:46;
A14: for y being set st y in dom (the Sorts of A * (the_arity_of o)) holds
g . y in (the Sorts of A * (the_arity_of o)) . y

proof

let y be set ; :: thesis: ( y in dom (the Sorts of A * (the_arity_of o)) implies g . y in (the Sorts of A * (the_arity_of o)) . y )
assume A15: y in dom (the Sorts of A * (the_arity_of o)) ; :: thesis: g . y in (the Sorts of A * (the_arity_of o)) . y
then A16: ( g . y in f . y & f . y in ((Class R) * (the_arity_of o)) . y ) by A4, A5, A12, A13;
reconsider n = y as Nat by A4, A6, A12, A13, A15, ORDINAL1:def 13;
reconsider s = (the_arity_of o) /. n as Element of S ;
A17: (the_arity_of o) . n = (the_arity_of o) /. n by A4, A6, A12, A13, A15, PARTFUN1:def 8;
then ((Class R) * (the_arity_of o)) . y = (Class R) . s by A4, A12, A13, A15, FUNCT_1:22
.= Class (R . s) by Def8 ;
then g . n in the Sorts of A . s by A16;
hence g . y in (the Sorts of A * (the_arity_of o)) . y by A15, A17, FUNCT_1:22; :: thesis: verum

end;

Args o,A = ((the Sorts of A # ) * the Arity of S) . o by MSUALG_1:def 9
.= product (the Sorts of A * (the_arity_of o)) by A2, MSAFREE:1 ;
then reconsider g = g as Element of Args o,A by A13, A14, CARD_3:18;

A18: now

let x be set ; :: thesis: ( x in dom (the_arity_of o) implies f . x = (R # g) . x )
assume A19: x in dom (the_arity_of o) ; :: thesis: f . x = (R # g) . x
then reconsider n = x as Nat by ORDINAL1:def 13;
reconsider s = (the_arity_of o) /. n as Element of S ;
f . n in Class (R . s) by A4, A6, A7, A19;
then consider a1 being set such that
A20: a1 in the Sorts of A . s and
A21: f . n = Class (R . s),a1 by EQREL_1:def 5;
g . n in f . n by A4, A6, A12, A19;
then Class (R . s),(g . n) = Class (R . s),a1 by A20, A21, EQREL_1:31;
hence f . x = (R # g) . x by A19, A21, Def9; :: thesis: verum

end;

take g ; :: thesis: x = R # g
dom (R # g) = dom ((Class R) * (the_arity_of o)) by CARD_3:18;
hence x = R # g by A3, A4, A6, A18, FUNCT_1:9; :: thesis: verum