defpred S1[ Nat, set ] means for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . $1 & h2 = the charact of U2 . $1 holds
$2 = [[:h1,h2:]];
set l = len the charact of U1;
set c = [: the carrier of U1, the carrier of U2:];
A2:
dom the charact of U2 = Seg (len the charact of U2)
by FINSEQ_1:def 3;
A3:
Seg (len the charact of U1) = dom the charact of U1
by FINSEQ_1:def 3;
A4:
for m being Nat st m in Seg (len the charact of U1) holds
ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x]
proof
let m be
Nat;
( m in Seg (len the charact of U1) implies ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x] )
assume A5:
m in Seg (len the charact of U1)
;
ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S1[m,x]
then reconsider f1 = the
charact of
U1 . m as non
empty homogeneous quasi_total PartFunc of
( the carrier of U1 *), the
carrier of
U1 by A3, MARGREL1:def 24;
len the
charact of
U1 = len the
charact of
U2
by A1, UNIALG_2:1;
then reconsider f2 = the
charact of
U2 . m as non
empty homogeneous quasi_total PartFunc of
( the carrier of U2 *), the
carrier of
U2 by A2, A5, MARGREL1:def 24;
reconsider F =
[[:f1,f2:]] as
Element of
PFuncs (
([: the carrier of U1, the carrier of U2:] *),
[: the carrier of U1, the carrier of U2:])
by PARTFUN1:45;
take
F
;
S1[m,F]
let h1 be non
empty homogeneous quasi_total PartFunc of
( the carrier of U1 *), the
carrier of
U1;
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . m & h2 = the charact of U2 . m holds
F = [[:h1,h2:]]let h2 be non
empty homogeneous quasi_total PartFunc of
( the carrier of U2 *), the
carrier of
U2;
( h1 = the charact of U1 . m & h2 = the charact of U2 . m implies F = [[:h1,h2:]] )
assume
(
h1 = the
charact of
U1 . m &
h2 = the
charact of
U2 . m )
;
F = [[:h1,h2:]]
hence
F = [[:h1,h2:]]
;
verum
end;
consider p being FinSequence of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) such that
A6:
dom p = Seg (len the charact of U1)
and
A7:
for m being Nat st m in Seg (len the charact of U1) holds
S1[m,p . m]
from FINSEQ_1:sch 5(A4);
reconsider p = p as PFuncFinSequence of [: the carrier of U1, the carrier of U2:] ;
take
p
; ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]] ) )
thus
len p = len the charact of U1
by A6, FINSEQ_1:def 3; for n being Nat st n in dom p holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]]
let n be Nat; ( n in dom p implies for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]] )
assume
n in dom p
; for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]]
hence
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
p . n = [[:h1,h2:]]
by A6, A7; verum