let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A being non-empty MSAlgebra over 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 over 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 over 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 1;
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 object 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₁[ object , object ] means $2 in f . $1;
A6: dom ((Class R) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
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 6;
then ((Class R) * (the_arity_of o)) . n = (Class R) . s by A4, A8, FUNCT_1:12
.= Class (R . s) by Def6 ;
hence f . n in Class (R . ((the_arity_of o) /. n)) by A4, A5, A8; :: thesis: verum

end;

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

proof

let a be object ; :: thesis: ( a in dom f implies ex b being object 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 object st S₁[a,b]
then reconsider n = a as Nat by A4, ORDINAL1:def 12;
f . n in Class (R . s) by A7, A10;
then consider a1 being object such that
A11: ( a1 in the Sorts of A . s & f . n = Class ((R . s),a1) ) by EQREL_1:def 3;
take a1 ; :: thesis: S₁[a,a1]
thus S₁[a,a1] by A11, EQREL_1:20; :: thesis: verum

end;

consider g being Function such that
A12: ( dom g = dom f & ( for a being object 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 2;
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:27;
A14: for y being object 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 object ; :: 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 A15, ORDINAL1:def 12;
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 6;
then ((Class R) * (the_arity_of o)) . y = (Class R) . s by A4, A12, A13, A15, FUNCT_1:12
.= Class (R . s) by Def6 ;
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:12; :: thesis: verum

end;

Args (o,A) = (( the Sorts of A #) * the Arity of S) . o by MSUALG_1:def 4
.= 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:9;

A18: now :: thesis: for x being object st x in dom (the_arity_of o) holds
f . x = (R # g) . x

let x be object ; :: 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 12;
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 object such that
A20: a1 in the Sorts of A . s and
A21: f . n = Class ((R . s),a1) by EQREL_1:def 3;
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:23;
hence f . x = (R # g) . x by A19, A21, Def7; :: thesis: verum

end;

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